**Property-Directed Shape Analysis**

*S. Itzhaky, N. Bjørner, T. Reps, M. Sagiv, and A. Thakur*

This paper addresses the problem of automatically generating
quantified invariants for programs that manipulate singly and doubly
linked-list data structures.
Our algorithm is *property-directed*—i.e., its choices are driven
by the properties to be proven.
The algorithm is able to establish that a correct program has no
memory-safety violations—e.g., null-pointer
dereferences, double frees—and that data-structure
invariants are preserved.
For programs with errors, the algorithm produces concrete counterexamples.

More broadly, the paper describes how to integrate IC3 with full predicate abstraction. The analysis method is complete in the following sense: if an inductive invariant that proves that the program satisfies a given property is expressible as a Boolean combination of a given set of predicates, then the analysis will find such an invariant. To the best of our knowledge, this method represents the first shape-analysis algorithm that is capable of (i)~reporting concrete counterexamples, or alternatively (ii)~establishing that the predicates in use are not capable of proving the property in question.

(Click here to access the paper: PDF; (c) Springer-Verlag.)