Clone wiki

jpf-bdd / Home


jpf-bdd is an extension of Java Pathfinder (JPF) that uses Binary Decision Diagrams (BDDs) to represent and explore parts of the state space of a Java program symbolically. In particular, it "replaces" the handling of a user-defined set of Boolean variables with a symbolic treatment. These variables will not be handled by jpf-core anymore. jpf-bdd will manage the values of the variables using BDDs. The main effect of jpf-bdd will be on the performance of the verification. On certain programs jpf-bdd improves both the runtime and the memory consumption of the verification procedure (compared to verification with jpf-core).


The tool jpf-bdd is used for experiments in various papers. We provide additional material for the interested readers at the following locations.

This published paper provides more information on the actual tool:

Wiki contents

  1. Installation (on this page)
  2. Acknowledgements (on this page)
  3. UserGuide
  4. Performance


To use jpf-bdd one needs a working installation of jpf-core. Installation instructions for jpf-core are available here:
Once jpf-core is installed you can download jpf-bdd, as follows:

$ hg clone

Then, jpf-bdd needs to be added as an extension to .jpf/ in your home directory. The file should look like this:

jpf-core = ${jpf-home}/jpf-core
jpf-bdd = ${jpf-home}/jpf-bdd

To build jpf-bdd, execute Ant in the jpf-bdd main directory:

cd jpf-bdd

Optionally you can execute the supplied j-unit tests:

cd jpf-bdd
ant test

In both cases the output should end with something like "BUILD SUCCESSFUL" which means that jpf-bdd was successfully build.


This project has been sponsored by Google (as a Google Summer of Code project). The project is maintained by Alexander von Rhein at the University of Passau, Germany. We are using the JProfiler Suite from ej-technologies for profiling and debugging JProfiler.