## Boolean Algebra of Shape Analysis Constraints

paper ps
The parametric shape analysis framework of Sagiv, Reps, and Wilhelm [45, 46] uses three-valued structures as dataflow lattice elements to represent sets of states at different program points. The recent work of Yorsh, Reps, Sagiv, Wilhelm [48, 50] introduces a family of formulas in (classical, two-valued) logic that are isomorphic to three-valued structures  and represent the same sets of concrete states. In this paper we introduce a larger syntactic class of formulas that has the same expressive power as the formulas in . The formulas in  can be viewed as a normal form of the formulas in our syntactic class; we give an algorithm for transforming our formulas to this normal form. Our formulas make it obvious that the constraints are closed under all boolean operations and therefore form a boolean algebra. Our algorithm also gives a reduction of the entailment and the equivalence problems for these constraints to the satisfiability problem.

### Citation

Viktor Kuncak and Martin Rinard. Boolean algebra of shape analysis constraints. In Verification, Model Checking and Abstract Interpretation, volume 2937 of LNCS, 2004.

### BibTex Entry

```@inproceedings{KuncakRinard04BooleanAlgebraShapeAnalysisConstraints,
author = {Viktor Kuncak and Martin Rinard},
title = {Boolean Algebra of Shape Analysis Constraints},
booktitle = {Verification, Model Checking and Abstract Interpretation},
series = {LNCS},
volume = {2937},
year = 2004,
abstract = {
The parametric shape analysis framework of Sagiv, Reps, and Wilhelm [45, 46] uses three-valued structures as dataflow lattice elements to represent sets of states at different program points. The recent work of Yorsh, Reps, Sagiv, Wilhelm [48, 50] introduces a family of formulas in (classical, two-valued) logic that are isomorphic to three-valued structures  and represent the same sets of concrete states.

In this paper we introduce a larger syntactic class of formulas that has the same expressive power as the formulas in . The formulas in  can be viewed as a normal form of the formulas in our syntactic class; we give an algorithm for transforming our formulas to this normal form. Our formulas make it obvious that the constraints are closed under all boolean operations and therefore form a boolean algebra. Our algorithm also gives a reduction of the entailment and the equivalence problems for these constraints to the satisfiability problem.
}
}
```