A lightweight symbolic execution technique for improving existing test suites by thoroughly checking for errors all sensitive operations executed by the test suite.


Software testing is an expensive and time consuming process, often involving the manual creation of comprehensive regression test suites. However, current testing methodologies do not take full advantage of these tests. In this paper, we present a technique for augmenting existing test suites using a lightweight symbolic execution mechanism, which thoroughly checks each sensitive operation executed by the test suite for errors, and explores additional paths around sensitive operations. We implemented this technique in a prototype system called ZESTI (Zero-Effort Symbolic Test Improvement), and show that it can find previously unknown bugs in several open-source applications, some of which are out of reach to standard symbolic execution. Our technique works transparently to the tester, requiring no additional human effort or changes to source code or tests.

Video Presentation

Watch a one minute video presentation to see the main idea behind our project.


A beta version is available for download. Use this version if you are interested to see how Zesti works or apply it to your code; it may still contain bugs and the documentation is currently scarce. For compilation, follow the same steps used when building KLEE, but instead of checking out KLEE, use the above Zesti distribution. More details are available on the Zesti Coreutils walkthrough page.

Research Support

This research project is generously sponsored by the UK EPSRC through a DTA studentship and the grant EP/J00636X/1.


  • make test-zesti: A Symbolic Execution Solution for Improving Regression Testing

    Paul Dan Marinescu, Cristian Cadar

    International Conference on Software Engineering (ICSE 2012)