Symbolically Computing Most-Precise Abstract Operations for Shape Analysis

Greta Yorsh, Thomas Reps and Mooly Sagiv

In Proc. Tools and Algorithms for the Construction and Analysis of Systems, 2004 (TACAS 2004)

Shape analysis concerns the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. This paper presents a new algorithm that takes as input a shape descriptor (describing some set of concrete stores X) and a precondition p, and computes the most-precise shape descriptor for the stores in X that satisfy p .

This algorithm solves several open problems in shape analysis:

The algorithm employs a theorem prover; termination can be assured by using standard techniques (e.g., having the theorem prover return a safe answer if a time-out threshold is exceeded) at the cost of losing the ability to guarantee that a most-precise result is obtained.

A prototype has been implemented in TVLA, using the SPASS theorem prover.

Click here to access the paper: PostScript, PDF.
Click here to acces the technical report: PostScript, PDF.