Shadow Symbolic Execution with Java PathFinder
This work addresses regression testing for Java developers, but it is incremental as it adapts an existing method from C to Java.
The authors tackled the problem of generating regression test cases for Java programs by applying shadow symbolic execution to Java bytecode using an extension of Java PathFinder, successfully generating test inputs that expose divergences in several test subjects.
Regression testing ensures that a software system when it evolves still performs correctly and that the changes introduce no unintended side-effects. However, the creation of regression test cases that show divergent behavior needs a lot of effort. A solution is the idea of shadow symbolic execution, originally implemented based on KLEE for programs written in C, which takes a unifed version of the old and the new program and performs symbolic execution guided by concrete values to explore the changed behavior. In this work, we apply the idea of shadow symbolic execution to Java programs and, hence, provide an extension of the Java PathFinder (JPF) project to perform shadow symbolic execution on Java bytecode. The extension has been applied on several subjects from the JPF test classes where it successfully generated test inputs that expose divergences relevant for regression testing.