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.)