Shape analysis concerns the problem of determining ``shape invariants'' for programs that perform destructive updating on dynamically allocated storage. In recent work, we have shown how shape analysis can be performed using an abstract interpretation based on 3-valued first-order logic. In that work, concrete stores are finite 2-valued logical structures, and the sets of stores that can possibly arise during execution are represented (conservatively) using a certain family of finite 3-valued logical structures. In this paper, we show how 3-valued structures that arise in shape analysis can be characterized using formulas in first-order logic with transitive closure.

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