DySy: dynamic symbolic execution for invariant inference

Dynamically discovering likely program invariants from con-crete test executions has emerged as a highly promising software engineering technique. Dynamic invariant infer-ence has the advantage of succinctly summarizing both “ex-pected”program inputs and the subset of program behaviors that is normal under those inputs. In this paper, we intro-duce a technique that can drastically increase the relevance of inferred invariants, or reduce the size of the test suite required to obtain good invariants. Instead of falsifying in-variants produced by pre-set patterns, we determine likely program invariants by combining the concrete execution of actual test cases with a simultaneous symbolic execution of conditions over program variables that the concrete tests satisfy during their execution. In this way, we obtain the benefits of dynamic inference tools like Daikon: the inferred invariants correspond to the observed program behaviors. At the same time, however, our inferred invariants are much more suited to the program at hand than Daikon’s hard-coded invariant patterns. The symbolic invariants are liter-ally derived from the program text itself, with appropriate value substitutions as dictated by symbolic execution. We implemented our technique in the DySy tool, which utilizes a powerful symbolic execution and simplification en-gine. The results confirm the benefits of our approach. In Daikon’s prime example benchmark, we infer the majority of the interesting Daikon invariants, while eliminating in-variants that a human user is likely to consider irrelevant