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.
This is joint work with Mooly Sagiv (Tel Aviv Univ.) and Reinhard Wilhelm (Univ. des Saarlandes). The talk will be based on a paper that will be given at the Twenty-Sixth ACM Symposium on Principles of Programming Languages (see http://www.cs.wisc.edu/wpis/papers/popl99.ps). (A somewhat more detailed treatment of the material is available at http://www.cs.wisc.edu/wpis/papers/tr1383.ps.)