Java Pathfinder (JPF) is a system to verify executable Java bytecode programs. JPF was developed at the NASA Ames Research Center and open sourced in 2005. The acronym JPF is not to be confused with the unrelated Java Plugin Framework project.
The core of JPF is a Java Virtual Machine that is also implemented in Java. JPF executes normal Java bytecode programs and can store, match and restore program states. Its primary application has been Model checking of concurrent programs, to find defects such as data races and deadlocks. With its respective extensions, JPF can also be used for a variety of other purposes, including
- model checking of distributed applications
- model checking of user interfaces
- test case generation by means of symbolic execution
- low level program inspection
- program instrumentation and runtime monitoring
JPF has no fixed notion of state space branches and can handle both data and scheduling choices.
Using the command line
~% cd /util/jpf/jpf-core/
jpf-core% java -jar build/RunJPF.jar src/examples/Racer.jpf
JavaPathfinder v6.0 - (C) RIACS/NASA Ames Research Center
.....
====================================================== statistics
elapsed time: 0:00:01
states: new=9, visited=1, backtracked=4, end=2
search: maxDepth=6, constraints hit=0
choice generators: thread=8 (signal=0, lock=1, shared ref=2), data=0
heap: new=336, released=32, max live=336, gc-cycles=7
instructions: 3200
max memory: 15MB
loaded code: classes=76, methods=1067
====================================================== search finished: 1/10/11 2:10 PM
- Bharat Jayaraman, instructor.
- Demian Lessa, instructor.
- http://en.wikipedia.org/wiki/Java_Pathfinder
- http://babelfish.arc.nasa.gov/trac/jpf
- http://babelfish.arc.nasa.gov/trac/jpf/wiki/install/build
