Shape analysis concerns the problem of determining ``shape invariants'' for programs that perform destructive updating on dynamically allocated storage. This paper presents a parametric framework for shape analysis that can be instantiated in different ways to create different shape-analysis algorithms that provide varying degrees of efficiency and precision.

A key innovation of the work is that the stores that can possibly arise during execution are represented (conservatively) using 3-valued logical structures. The framework is instantiated in different ways by varying the predicates used in the 3-valued logic. The class of programs to which a given instantiation of the framework can be applied is not limited a priori (i.e., as in some work on shape analysis, to programs that manipulate only lists, trees, dags, etc.); each instantiation of the framework can be applied to any program, but may produce imprecise results (albeit conservative ones) due to the set of predicates employed.

[paper: PostScript, PDF; talk: Powerpoint]