Shape Analysis through Predicate Abstraction and Model Checking

We propose a new framework, based on predicate abstraction and model checking, for shape analysis of programs. Shape analysis is used to statically collect information -- such as possible reachability and sharing -- about program stores. Rather than use a specialized abstract interpretation based on shape graphs, we instantiate a generic and automated abstraction procedure with shape predicates from a correctness property. This procedure identifies predicates relevant for correctness, using an analysis based on weakest preconditions, and creates a finite state abstract program. The correctness property is then checked on the abstraction with a model checking tool. To enable this process, we calculate weakest preconditions for common shape properties, and present heuristics for accelerating convergence.