A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs

Jesse Bingham, Zvonimir Rakamaric. 7th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2006), Charleston, SC, USA.
[pdf] [bib]

Abstract: An important and ubiquitous class of programs are heap-manipulating programs (HMP), which manipulate unbounded linked data structures by following pointers and updating links. Predicate abstraction has proved to be an invaluable technique in the field of software model checking; this technique relies on an efficient decision procedure for the underlying logic. The expression and proof of many interesting HMP safety properties require transitive closure predicates; such predicates express that some node can be reached from another node by following a sequence of (zero or more) links in the data structure. Unfortunately, adding support for transitive closure often yields undecidability, so one must be careful in defining such a logic. Our primary contributions are the definition of a simple transitive closure logic for use in predicate abstraction of HMPs, and a decision procedure for this logic. Through several experimental examples, we demonstrate that our logic is expressive enough to prove interesting properties with predicate abstraction, and that our decision procedure provides us with both a time and space advantage over previous approaches.

Errata: After the paper was published, we found a bug in the implementation which slightly changes our experimental results. Our tech-report presents corrected results and adds proofs to the published version.

Bibtex:

@inproceedings{vmcai2006-br,
  author = {Jesse Bingham and Zvonimir Rakamari\'c},
  title = {A Logic and Decision Procedure for Predicate
    Abstraction of Heap-Manipulating Programs},
  booktitle = {Proceedings of the 7th International Conference on
    Verification, Model Checking and Abstract Interpretation
    (VMCAI 2006)},
  series = {Lecture Notes in Computer Science},
  volume = {3855},
  publisher = {Springer},
  editor = {E. Allen Emerson and Kedar S. Namjoshi},
  year = {2005},
  pages = {207--221},
}