Parametric Shape Analysis via 3-Valued Logic
Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm
We present a family of abstract-interpretation algorithms that are capable of determining ``shape invariants'' of programs that perform destructive updating on dynamically allocated storage. The main idea is to represent the stores that can possibly arise during execution using three-valued logical structures.
Questions about properties of stores can be answered by evaluating predicate-logic formulae using Kleene's semantics of three-valued logic:
The approach described is a parametric framework: It provides the basis for generating a family of shape-analysis algorithms by varying the vocabulary used in the three-valued logic.
(Click here to access the paper: PostScript, PDF.)