Sciweavers

Share
FOSSACS
2006
Springer

A Logic of Reachable Patterns in Linked Data-Structures

10 years 2 months ago
A Logic of Reachable Patterns in Linked Data-Structures
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 preconditions, 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 the entry of a procedure to the field on the exit of a procedure. Therefore, it is possible to ...
Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sag
Added 22 Aug 2010
Updated 22 Aug 2010
Type Conference
Year 2006
Where FOSSACS
Authors Greta Yorsh, Alexander Moshe Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani
Comments (0)
books