R.: Logical characterizations of heap abstractions

Abstract. Shape analysis concerns the problem of determining “shape invariants ” for pro-grams 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 struc-tures, and the sets of stores that can possibly arise during execution are represented (conser-vatively) 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. We also define a non-standard (“supervaluational”) semantics for 3-valued first-order logic that is more precise than a conventional 3-valued semantics, and demonstrate that the supervaluational semantics can be implemented using existing theorem provers.