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:

Three-valued logical structures are thus a conservative representation of memory stores.

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.)