Combines dynamic symbolic execution with several novel heuristics based on program analysis to automatically and comprehensively test code patches.


One of the distinguishing characteristics of software systems is that they evolve: new patches are committed to software repositories and new versions are released to users on a continuous basis. Unfortunately, many of these changes bring unexpected bugs that break the stability of the system or affect its security. KATCH addresses this problem using a technique for automatic and comprehensive testing of code patches. It combines symbolic execution with several novel heuristics based on static and dynamic program analysis, and leverages existing test suites to quickly reach the new code.

KATCH received a Distinguished Artifact award at ESEC/FSE 2013.


The source code of KATCH is available at Since KATCH is based on KLEE, you can use the same instructions used to compile KLEE at the timeā€”for instance, see

Research Support

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


  • KATCH: High-Coverage Testing of Software Patches

    Paul Dan Marinescu, Cristian Cadar

    European Software Engineering Conference / ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2013)

  • High-Coverage Symbolic Patch Testing

    Paul Dan Marinescu, Cristian Cadar

    International SPIN Workshop on Model Checking of Software (SPIN 2012)