Property-directed shape analysis

Abstract. This paper addresses the problem of automatically generating quan-tified 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 pro-gram 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 ab-straction. 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.