*Property-Directed Shape Analysis*

Itzhaky, Shachar and Bjørner, Nikolaj and Reps, Thomas W. and Sagiv, Mooly and Thakur, Aditya V.26th International Conference on Computer Aided Verification (CAV), 2014

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.

PDF Springer©@inproceedings{itzhaky_etal_CAV14, author = {Itzhaky, Shachar and Bj{\o}rner, Nikolaj and Reps, Thomas W. and Sagiv, Mooly and Thakur, Aditya V.}, title = {Property-Directed Shape Analysis}, booktitle = {26th International Conference on Computer Aided Verification ({CAV})}, year = {2014}, pages = {35--51}, doi = {10.1007/978-3-319-08867-9_3}, publisher = {Springer} }