Model Checking

Model checking gives us an algorithmic means to determine whether an abstract model, which represents, for example, a Java program, satisfies a property expressed in a particular logic. In case the property is not satisfied, it identifies a counterexample that shows why the property does not hold.

Java PathFinder

Java PathFinder (JPF) is a model checker to verify properties of Java bytecode. In its basic form, it is a Java virtual machine. In contrast to an ordinary Java virtual machine, JPF systematically explores all potential execution paths of a program, rather than a single one. While exploring those execution paths, JPF tries to find violations of properties like uncaught exceptions and deadlocks. More information about JPF can be found at the URL http://babelfish.arc.nasa.gov/trac/jpf/. JPF has been developed in such a way that it can be easily extended. Our group has developed a number of extension of JPF. Some details are provided below.

Detecting Data Races with JPF

Roughly speaking, a (data) race on a shared variable arises in a concurrent program if two threads access that variable simultaneously and the accesses are conflicting, that is, at least one of them writes to the variable. Although some races are benign, races often are an indication of bugs. Hence, tools that detect them are invaluable to those writing concurrent programs. In collaboration with Willem Visser (NASA), graduate students Sergei Kulikov and Nastaran Shafiei have developed an extension to JPF that detects races. The extension is part of the standard distribution of JPF.

Handling Invocations of Native Code within JPF

JPF provides a way to handle invocations of native code. However, in the current implementation only some classes of the Java standard library with native calls are handled. To handle any other classes that contain native calls, one should have a low level understanding of the Java class and the internal features of JPF. That limits the use of JPF. Graduate student Nastaran Shafiei has developed an extension of JPF that handles invocations of native code is a systematic and automatic way.

Probabilistic Model Checking with JPF

Graduate student Xin Zhang has extended JPF to a probabilistic model checker. This allows us to use probabilistic information while model checking Java code where probabilities are assigned to some choices (think, for example, of the different possible outcomes of the nextInt(int) method of the Random class).