Local data structure invariants are asserted over a bounded fragment of a data structure around a distinguished node M of the data structure. An example of such an invariant for a sorted doubly linked list is "for all nodes M of the list, if M ≠ null and M.next ≠ null, then M.next.prev = M and M.value ≤ M.next.value." It has been shown that such local invariants are both natural and sufficient for describing a large class of data structures. This paper explores a novel technique, called Krystal, to infer likely local data structure invariants using a variant of symbolic execution, called universal symbolic execution. Universal symbolic execution is like traditional symbolic execution except the fact that we create a fresh symbolic variable for every read of a lvalue that has no mapping in the symbolic state rather than creating a symbolic variable only for inputs. This helps universal symbolic execution to symbolically track data flow for all memory locations along an execution even if input values do not flow directly into those memory locations. We have implemented our algorithm and applied it to several data structure implementations in Java. Our experimental results show that we can infer many interesting local invariants for these data structures.

We consider the problem if a given program satisfies a specified safety property. Interesting programs have infinite state spaces, with inputs ranging over infinite domains, and for these programs the property checking problem is undecidable. Two broad approaches to property checking are testing and verification. Testing tries to find inputs and executions which demonstrate violations of the property. Verification tries to construct a formal proof which shows that all executions of the program satisfy the property. Testing works best when errors are easy to find, but it is often difficult to achieve sufficient coverage for correct programs. On the other hand, verification methods are most successful when proofs are easy to find, but they are often inefficient at discovering errors. We propose a new algorithm, Synergy, which combines testing and verification. Synergy unifies several ideas from the literature, including counterexample-guided model checking, directed testing, and partition refinement.This paper presents a description of the Synergy algorithm, its theoretical properties, a comparison with related algorithms, and a prototype implementation called Yogi.