Boolean Algebra of Shape Analysis Constraints

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 s...

• Type: Conference
• Year: 2004
• Where: VMCAI
• Authors: Viktor Kuncak, Martin C. Rinard
• Keywords: Shape Analysis, Shape Analysis Constraints, Software Engineering, Three-valued Structures, VMCAI 2004