Boolean Algebra of Shape Analysis Constraints

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 [46] and represent the same sets of concrete states.