The goal of shape analysis is to analyze properties of programs that perform
destructive updates of linked structures (heaps). This thesis
presents an approach for shape analysis based on program augmentation
(instrumentation), predicate abstraction, and model checking, that
verification of safety and liveness properties (which, for sequential
usually corresponds to program invariance and termination).
One of the difficulties in abstracting heap-manipulating programs is devising a decision procedure for a sufficiently expressive logic of graph properties. Since graph reachability (expressible by transitive closure) is not a first order property, the challenge is in showing that a decision procedure exists for a rich enough subset of first order logic with transitive closure.
Predicate abstraction is in general too weak to verify liveness properties. Thus an additional issue dealt with is how to perform abstraction while retaining enough information. The method presented here is domain-neutral, and applies to concurrent programs as well as sequential ones.