Precise and compact modular procedure summaries for heap manipulating programs

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. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification General Terms Languages, Verification, Experimentation

• Type: Journal
• Year: 2011
• Where: PLDI
• Authors: Isil Dillig, Thomas Dillig, Alex Aiken, Mooly Sagiv
• Keywords: Analysis Algorithm, Decompositions, PLDI 2011, Programming Languages, Subject Descriptors