[ list |
abstracts |
bib ]

## On the Boolean Algebra of Shape Analysis Constraints

paper pdf
paper ps
### Abstract

Shape analysis is a promising technique for statically
verifying and extracting properties of programs that
manipulate complex data structures. We introduce a new
characterization of constraints that arise in parametric
shape analysis based on manipulation of three-valued
structures as dataflow facts.
We identify an interesting syntactic class of first-order
logic formulas that captures the meaning of three-valued
structures under concretization. This class is broader than
previously introduced classes, allowing for a greater
flexibility in the formulation of shape analysis constraints
in program annotations and internal analysis
representations. Three-valued structures can be viewed as
one possible normal form of the formulas in our class.
Moreover, we characterize the meaning of three-valued
structures under “tight concretization”. We show that the
seemingly minor change from concretization to tight
concretization increases the expressive power of
three-valued structures in such a way that the resulting
constraints are closed under all boolean operations. We
call the resulting constraints *boolean shape analysis
constraints*.
The main technical contribution of this paper is a natural
syntactic characterization of boolean shape analysis
constraints as arbitrary boolean combinations of
first-order sentences of certain form, and an algorithm for
transforming such boolean combinations into the normal
form that corresponds directly to three-valued structures.
Our result holds in the presence of arbitrary shape analysis
instrumentation predicates. The result enables the
reduction (without any approximation) of the entailment and
the equivalence of shape analysis constraints to the
satisfiability of shape analysis constraints. When the
satisfiability of the constraints is decidable, our result
implies that the entailment and the equivalence of the
constraints are also decidable, which enables the use of
constraints in a compositional shape analysis with a
predictable behavior.

### Citation

Viktor Kuncak and Martin Rinard.
On the boolean algebra of shape analysis constraints.
Technical report, MIT CSAIL, August 2003.### BibTex Entry

@TECHREPORT{KuncakRinard03OnBooleanAlgebraShapeAnalysisConstraints,
author = {Viktor Kuncak and Martin Rinard},
title = {On the Boolean Algebra of Shape Analysis Constraints},
institution = {MIT CSAIL},
year = 2003,
month = {August},
localurl = {http://lara.epfl.ch/~kuncak/papers/KuncakRinard03OnBooleanAlgebraShapeAnalysisConstraints.pdf}
}

[ list |
abstracts |
bib ]