A Model Checker for Java Programs
Recipient of NASA's 2003 TGIR Award for Engineering Innovation
JPF is now available at SourceForge (Non-NASA Link!)
The majority of work carried out in the formal methods community
throughout the last three decades has (for good reasons) been devoted
to special languages designed to make it easier to experiment with
mechanized formal methods such as theorem provers and model
checkers. We believe it is time for the formal methods community to
shift some of its attention towards the analysis of programs written
in modern programming languages.
In keeping with this philosophy we have developed a verification
and testing environment for Java which integrates model checking,
program analysis and testing - called Java PathFinder (JPF). JPF
consists of a custom-made Java Virtual Machine (JVM) that interprets
bytecode combined with a search interface to allow the complete
behavior of a Java program to be analyzed (including all interleavings
of concurrent programs). JPF is implemented in Java and its
architecture is highly modular to support rapid prototyping of new
JPF is a so-called explicit-state model checker, since it enumerates
all visited states, and therefore suffers from the state-explosion
problem inherent in analyzing large programs. It is ideally suited to
analyzing programs less than 10kLOC, but has been successfully applied
to finding errors in concurrent programs up to 100kLOC.
JPF has the following list of main features:
- Works at the bytecode level, hence all of Java can be
model checked as well as errors that can only be found on the
bytecode level can be uncovered.
- By default it checks for all runtime errors (uncaught exceptions),
assertion violations (supports Java's assert), and deadlocks. Although
JPF previously supported LTL checking this feature has been
- Contains garbage collection, since a typical Java program will
be infinite-state without garbage collection (state size will grow
- Use symmetry reductions of the heap during model checking to reduce
- Use dynamic partial-order reductions to reduce the number of
- Supports BFS and DFS search as well as heuristic based search, e.g.
A*, Best-First, etc.
- Contains a run-time analysis mode that uses the Eraser algorithm
to find race-conditions as well as a Lock Order analysis to check
whether locks can be taken in different orders (which often leads to
deadlocks). The results of the run-time analysis can be used to
guide JPF towards errors.
- Includes the capability to do symbolic execution of Java programs,
including symbolic execution of complex data (such as linked lists and
- Supports the calculation of structural coverage (branch and
statement coverage) during model checking; coverage can also guide
- Facility to explain the real cause of an error the tool finds.
- Allows the creation of listeners that can subscribe to events
during the search - this facility makes JPF easily extensible.
- Supports the creation of dedicated code to be executed in place of
regular classes - this allows one to easily handle native calls
and improve the efficiency of the analysis.