A Decidable Logic for Describing Linked Data Structures

Michael Benedikt, Thomas Reps, and Mooly Sagiv

This paper aims to provide a better formalism for describing properties of linked data structures (e.g., lists, trees, graphs), as well as the intermediate states that arise when such structures are destructively updated. The paper defines a new logic that is suitable for these purposes (called Lr, for ``logic of reachability expressions''). We show that Lr is decidable, and explain how Lr relates to two previously defined structure-description formalisms (``path matrices'' and ``static shape graphs'') by showing how an arbitrary shape descriptor from each of these formalisms can be translated into an Lr formula.

(Click here to access the paper: PostScript, PDF.)