, a new technique for proving properties of heap-manipulating programs that marries (1) a new
analysis for heap reasoning with (2) an
technique for refining heap-shape invariants with data invariants.
, and produces counterexample traces when a property does not hold. Using the novel notion of
spatial interpolants modulo theories
can infer complex invariants over general recursive predicates, e.g., of the form
all elements in a linked list are even
binary tree is sorted
. Furthermore, we treat interpolation as a black box, which gives us the freedom to encode data manipulation in any suitable theory for a given program (e.g., bit vectors, arrays, or linear arithmetic), so that our technique immediately benefits from any future advances in SMT solving and interpolation.