Introducing Binary Decision Diagrams in the explicit-state verification of Java code

One of the big performance problems of software model checking is the state-explosion problem. Various tools exist to tackle this problem. One of such tools is Java Pathfinder (JPF) an explicit-state model checker for Java code that has been used to verify efficiently a number of real applications. We present jpf-bdd, a JPF extension that allows users to annotate Boolean variables in the system under test to be managed using Binary Decision Diagrams (BDDs). Our tool partitions the program states of the system being verified and manages one part using BDDs. It maintains a formula for the values of these state partitions at every point during the verification. This allows us to merge states that would be kept distinct otherwise, thereby reducing the effect of the state-explosion problem. We demonstrate the performance improvement of our extension by means of three example programs including an implementation of the well-known dining- philosophers problem