A Logic of Reachable Patterns in Linked Data-Structures
Greta
Yorsh, Alexander Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani
In Proc. Foundations of Software Science and Computation Structures,
2006 (FOSSACS 2006)
We define a new decidable logic for expressing
and checking invariants of programs that manipulate dynamically-allocated
objects via pointers and destructive pointer updates. The main feature of this
logic is the ability to limit the neighborhood of a node that is reachable via
a regular expression from a designated node. The logic is closed under boolean
operations (entailment, negation) and has a finite model property. The key
technical result is the proof of decidability. We show how to express
precondition, postconditions, and loop invariants for some interesting
programs. It is also possible to express properties such as disjointness of
data-structures, and low-level heap mutations. Moreover, our logic can express
properties of arbitrary data-structures and of an arbitrary number of pointer
fields. The latter provides a way to naturally specify postconditions that
relate the fields on entry to a procedure to the fields on exit. Therefore, it
is possible to use the logic to automatically prove partial correctness of
programs performing low-level heap mutations.
Click here to access the full version of the paper (including proofs),
published at JLAP:
PDF