This project is read-only.

Welcome to DySy

DySy is a fully automated tool that uses dynamic symbolic execution (Pex) for invariant inference

Abstract

Dynamically discovering likely program invariants from concrete test executions has emerged as a highly promising software engineering technique. Dynamic invariant inference has the advantage of succinctly summarizing both "expected" program inputs and the subset of program behaviors that is normal under those inputs. Here, we introduce 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 invariants 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 the same tests. The symbolic execution produces abstract 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 literally 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 engine. 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 invariants that a human user is likely to consider irrelevant.

Comparison with Daikon

Daikon has pioneered the field of dynamic invariant detection. We compare DySy with Daikon.

Download

Download DySy--it's free.

Usage

Using DySy is easy.

Technical Papers

  • The DySy paper appeared in the Proceedings of the 30th ACM/IEEE International Conference on Software Engineering (ICSE), May 2008.

Credits

The following people have helped us by sending us great feedback, bug reports, etc.
  • Brian Strelioff
  • Jiangfan
  • Michael Ernst
  • Nadya Kuzmina
  • Peli de Halleux
  • Reid Hochstedler
  • Thank you also to the people we forgot to acknowledge here. Please remind us by email to add you.

People

Last edited Nov 20, 2008 at 11:24 PM by csallner, version 10

Comments

No comments yet.