An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures

Zvonimir Rakamaric, Jesse Bingham, Alan J. Hu. 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007), Nice, France.
[pdf] [bib]

Abstract: Research on the automatic verification of heap-manipulating programs (HMPs)—programs that manipulate unbounded linked data structures via pointers—has blossomed recently, with many different approaches all showing leaps in performance and expressiveness. A year ago, we proposed a small logic for specifying predicates about HMPs and demonstrated that an inference-rule-based decision procedure could be performance-competitive, and in many cases superior to other methods known at the time. That work, however, was a proof-of-concept, with a logic fragment too small to verify most real programs. In this work, we generalize our previous results to be practically useful: we allow the data in heap nodes to be mutable, we allow more than a single pointer field, and we add new primitives needed to verify cyclic structures. Each of these extensions necessitates new or changed inference rules, with the concomitant changes to the proofs and decision procedure. Yet, our new decision procedure, with the more general logic, actually runs as fast as our previous results. With these generalizations, we can automatically verify many more HMP examples, including three small container functions from the Linux kernel.

Bibtex:

@inproceedings{vmcai2007-rbh,
  author = {Zvonimir Rakamari\'c and Jesse Bingham and Alan J. Hu},
  title = {An Inference-Rule-Based Decision Procedure for Verification
    of Heap-Manipulating Programs with Mutable Data and Cyclic Data
    Structures},
  booktitle = {Proceedings of the 8th International Conference on
    Verification, Model Checking and Abstract Interpretation
    (VMCAI 2007)},
  series = {Lecture Notes in Computer Science},
  volume = {4349},
  publisher = {Springer},
  editor = {Byron Cook and Andreas Podelski},
  year = {2007},
  month = {January},
  pages = {106--121},
}