Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
This is a description of changes made for my participation in the Google Summer of Code 2017 project. I worked on integrating veritesting with Symbolic PathFinder.

GSoC Project abstract

Work summary

During summer of 2017, I worked on a Google Summer of Code project for implementing a technique called Veritesting in Symbolic PathFinder. For the static analysis part of veritesting, I created a Soot extension which automatically generates the main listener function of Symbolic PathFinder.


Veritesting requires static symbolic execution to be performed, when possible, to exponentially reduce the number of execution paths required for complete path exploration in symbolic execution. To integrate veritesting with Symbolic PathFinder, I created a Soot extension which needs to be run as a prior step to a symbolic execution with SPF. Running this step will produce a collection of executeInstruction functions that SPF can run. My veritesting implementation currently causes symbolic execution of the following code to have one execution path instead of 4, when x and y are marked as symbolic integers.

    if (x <= 800 ) a = -1; 
    else a = 1;
    if (y <= 1200 ) b = -1; 
    else b = 1;

This integration also required SPF to have complex constraints involving multiple comparison operators. I implemented these changes to allow SPF to solve such complex constraints (see To solve such constraints, I implemented support for SPF to communicate these constraints with the Z3BitVector solver.

The project was maintained here. The project is in usable state. The complete example for which my veritesting implementation works is here. My Soot extension can be found in jpf-symbc/src/examples/ and my auto-generated listener functions can be found in jpf-symbc/src/main/gov/nasa/jpf/symbc/

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.