Parametric shape analysis via 3-valued logic

Abstract

Shape analysis concerns the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. This article 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. Categories and Subject Descriptors: D.2.5 [Software Engineering]: Testing and Debugging -symbolic execution; D.3.3 [Programming Languages]: Language Constructs and Features -data types and structures; dynamic storage management; E.1 [Data]: Data Structures - graphs; lists; trees; E.2 [Data]: Data Storage Representations - composite structures; linked representations; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs - assertions; invariants.