Heap Memory Requirements Analysis via Separation Logic
(0) Memory is a constrained resource for software, and memory consumption is an essential factor to evaluate a programs 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 programs 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.
Guanhua He Chenguang Luo
Department of Computer Science Durham University Durham, UK
国际会议
天津
英文
321-322
2009-07-29（万方平台首次上网日期，不代表论文的发表时间）