jpf-bdd, A jpf project for handling Boolean variables with Binary Decision Diagrams

by rhein for The Java Pathfinder Team

This project aims at extending the model checker Java Path Finder to handle a special set of Boolean variables using Binary Decision Diagrams (BDDs). This enables efficient verification of Java programs with a set of Boolean variables that are guiding the control flow. In this project I will use software product-lines as a concrete example for such programs. Verification of a product-line with JPF and the BDD-extension will be significantly faster than with a standard JPF-installation.