Property-Directed Shape Analysis
File(s)
Date
2014-05-22Author
Itzhaky, Shachar
Bjorner, Nikolaj
Reps, Thomas
Sagiv, Mooly
Thakur, Aditya
Metadata
Show full item recordAbstract
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 -- i.e., there are no 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 is not capable of proving the property in question.
Subject
shape analysis
predicate abstraction
program verification
Permanent Link
http://digital.library.wisc.edu/1793/69022Citation
TR1807