ShadowJPF (jpf-shadow) is an extension of the Java PathFinder (JPF) [1,2] and applies the idea of shadow symbolic execution [3] to Java bytecode and, hence, allows to detect divergences in Java programs that expose new program behavior.

This tool was presented in "Shadow Symbolic Execution with Java PathFinder" at the Java PathFinder Workshop 2017 workshop co-located with the ASE. For more information please have a look at our workshop paper published in the ACM SIGSOFT Software Engineering Notes.

Authors: Yannic Noller, Hoang Lam Nguyen, Minxing Tang, and Timo Kehrer

_{[1] W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda. Model checking programs. Automated Software Engineering, 10(2):203–232, Apr 2003. https://doi.org/10.1023/A:1022920129859
[2] C. S. Pasareanu, W. Visser, D. Bushnell, J. Geldenhuys, P. Mehlitz, and N. Rungta. Symbolic pathfinder: integrating symbolic execution with model checking for java bytecode analysis. Automated Software Engineering, 20(3):391–425, 2013. https://doi.org/10.1007/s10515-013-0122-2
[3] Hristina Palikareva, Tomasz Kuchta, and Cristian Cadar. 2016. Shadow of a doubt: testing for divergences between software versions. In Proceedings of the 38th International Conference on Software Engineering (ICSE '16). ACM, New York, NY, USA, 1181-1192. https://doi.org/10.1145/2884781.2884845}

The following instructions will show you how to install and run jpf-shadow.

jpf-shadow is built as an extension of Symbolic Pathfinder (SPF) (which is again build on top of Java Pathfinder(JPF)). Therefore, make sure to have jpf-core and jpf-symbc installed and properly setup on your machine.

Assuming that you have installed jpf-core, jpf-symbc and jpf-shadow under <user.home>/workspace/jpf, your site.properties file (usually located in <user.home>/.jpf) should look like this:

# JPF site configuration

jpf-core = ${user.home}/workspace/jpf/jpf-core
jpf-symbc = ${user.home}/workspace/jpf/jpf-symbc
jpf-shadow = ${user.home}/workspace/jpf/jpf-shadow

extensions=${jpf-core},${jpf-symbc},${jpf-shadow}

To build jpf-shadow using the command line, move to the project directory (i.e. <user.home>/workspace/jpf/jpf-shadow) and run:

ant build

If there are any building errors, please check if your site.properties file is setup correctly.

1. In Eclipse, go to File > Import... to import jpf-shadow as an existing project.
2. Confirm that jpf-core and jpf-symbc are listed as required projects on the build path of jpf-shadow.
3. Select the build.xml file and run it as Ant Build.

To run a change()-annotated Java program, jpf-shadow requires an appropriate .jpf configuration file. The folder src/examples contains various examples of annotated programs together with their .jpf files.

The settings that can be specified are:

The Foo example from the paper (located inside src/examples/jpf2017) can now be executed in the following way:

To specify the initial test input of the foo(int) method, simply change the concrete parameter passed to it inside the main method.

Use the command:

java -jar <user.home>/workspace/jpf/jpf-core/build/RunJPF.jar <user.home>/workspace/jpf/jpf-shadow/src/examples/jpf2017/foo/Foo.jpf

Select the Foo.jpf configuration file and run it using the run-jpf-shadow run configuration.

Assuming that foo(int) has been run with the initial input x=1, the output should contain the following lines:

...
====================================================== Method Summaries
Inputs: x

jpf2017.foo.Foo_1c.foo(11)	--> Diff in line: 22, Type: diffFalse	(Return Value: 2)
Paths explored: 1
...

This means that jpf-shadow has found a diff false divergence (i.e. the old version takes the true path while the new version takes the false path) at line 22 for the input x=11 and the return value (of the new version) is 2.