Java Pathfinder

Java Pathfinder 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. 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.

Extensibility

JPF is an open system that can be extended in a variety of ways. The main extension constructs are

listeners - to implement complex properties
peer classes - to execute code at the host JVM level, which is mostly used to implement native methods
bytecode factories - to provide alternative execution semantics of bytecode instructions
choice generators - to implement state space branches such as scheduling choices or data value sets
serializers - to implement program state abstractions
publishers - to produce different output formats
search policies - to use different program state space traversal algorithms

JPF includes a runtime module system to package such constructs into separate JPF extension projects. A number of such projects are available from the main JPF server, including a symbolic execution mode, numeric analysis, race condition detection for relaxed memory models, user interface model checking and many more.

Limitations

JPF cannot analyze Java native methods. If the system under test calls such methods, these have to be provided within peer classes, or intercepted by listeners
as a model checker, JPF is susceptible to Combinatorial explosion, although it performs on-the-fly Partial order reduction
the configuration system for JPF modules and runtime options can be complex