Skip to Main content Skip to Navigation
Journal articles

A Logic of Reachable Patterns in Linked Data-Structures

Abstract : 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 procedure's entry to the field on procedure's exit. Therefore, it is possible to use the logic to automatically prove partial correctness of programs performing low-level heap mutations.
Document type :
Journal articles
Complete list of metadata

Cited literature [46 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-00681203
Contributor : Antoine Meyer <>
Submitted on : Tuesday, March 20, 2012 - 9:54:11 PM
Last modification on : Thursday, November 19, 2020 - 11:48:02 AM
Long-term archiving on: : Thursday, June 21, 2012 - 2:55:42 AM

File

paper.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Greta Yorsh, Alexander Rabinovich, Mooly Sagiv, Antoine Meyer, Ahmed Bouajjani. A Logic of Reachable Patterns in Linked Data-Structures. Journal of Logic and Algebraic Programming, Elsevier, 2007, 73 (1-2), p. 111-142. ⟨10.1016/j.jlap.2006.12.001⟩. ⟨hal-00681203⟩

Share

Metrics

Record views

352

Files downloads

604