| The goal of shape analysis is to analyze properties of programs that perform destructive updating on dynamically allocated storage (heaps). In the past decade various frameworks have been proposed, most notable being the line of work based on shape graphs and canonical abstraction [SRW99, LAS00]. Frameworks have been proposed since, among them based on counter automata, predicate abstraction, and separation logic. However, among these examples there has been little effort in dealing with liveness properties (e.g., termination) of systems whose verification depends on deep heap properties (a notable exception being [BCDO06]).; This dissertation presents a new shape analysis framework that is based on predicate abstraction, program augmentation, and model checking. The combination of predicate abstraction and program augmentation is collectively known as Ranking Abstraction, and provides a sufficiently powerful model for verification of liveness properties of sequential and concurrent systems. Furthermore, a new predicate abstraction method is presented, that allows for automatic computation of abstract systems that does not rely on theorem provers. This approach has several intrinsic limitations, most notably on the class of analyzable heap shapes. Thus several extensions are described that allow for complex heap shapes. |
