Heap Memory Requirements Analysis via Separation Logic

Memory is a constrained resource for software, and memory consumption is an essential factor to evaluate a program´s performance. Therefore, there are existing works which concentrated on the inference of programs´ memory usage. However, previous works mainly exploited type systems to infer programs´ memory consumption, which were weak at handling aliasing information for heap manipulating programs. In this work, we propose an automated inference system for programs´ memory usage based on the framework of Nguyen et al. The system can capture both the maximum requirement and the net usage of memory. We employ a separation logic based forward analysis to track the program´s execution symbolically, and use symbolic Presburger arithmetic expressions to express the effect of allocation and deallocation in heap memory. Our approach is sound, and is also expected to provide more precision and scalability than previous works.