Parametric Shape Analysis via 3-Valued Logic

Parametric Shape Analysis via 3-Valued Logic

March 2000 (Revised) | Mooly Sagiv, Thomas Reps, Reinhard Wilhelm
This paper presents a family of abstract interpretation algorithms for determining "shape invariants" in programs that perform destructive updating on dynamically allocated storage. The key innovation is the use of 3-valued logical structures to represent possible stores during execution. Questions about store properties can be answered by evaluating predicate-logic formulae using Kleene's 3-valued semantics, which provides a conservative representation of memory stores. The paper introduces a parametric framework for shape analysis, which allows different shape graphs to be generated by varying the predicates used in the 3-valued logic. This framework can handle every program but may produce conservative results due to the class of predicates used. The paper also discusses the use of logic in shape analysis, the representation of stores via 3-valued structures, and the embedding of 2-valued logic into 3-valued logic. The authors demonstrate the effectiveness of their approach through examples and show how it can be used to improve the precision of shape analysis for programs that manipulate linked data structures.This paper presents a family of abstract interpretation algorithms for determining "shape invariants" in programs that perform destructive updating on dynamically allocated storage. The key innovation is the use of 3-valued logical structures to represent possible stores during execution. Questions about store properties can be answered by evaluating predicate-logic formulae using Kleene's 3-valued semantics, which provides a conservative representation of memory stores. The paper introduces a parametric framework for shape analysis, which allows different shape graphs to be generated by varying the predicates used in the 3-valued logic. This framework can handle every program but may produce conservative results due to the class of predicates used. The paper also discusses the use of logic in shape analysis, the representation of stores via 3-valued structures, and the embedding of 2-valued logic into 3-valued logic. The authors demonstrate the effectiveness of their approach through examples and show how it can be used to improve the precision of shape analysis for programs that manipulate linked data structures.
Reach us at info@study.space
Understanding Parametric shape analysis via 3-valued logic