Precise and compact modular procedure summaries for heap manipulating programs
Işıl Dillig, Thomas Dillig, Alex Aiken, Mooly Sagiv · ACM SIGPLAN Notices · 2011
We present a strictly bottom-up, summary-based, and precise heap analysis targeted for program verification that performs strong updates to heap locations at call sites. We first present a theory of heap decompositions that forms the basis of our approach; we then describe a full analysis algorithm that is fully symbolic and efficient. We demonstrate the precision and scalability of our approach for verification of real C and C++ programs.