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

Example 
The following system under test contains a simple race condition between two threads accessing the same variable d in statements (1) and (2), which can lead to a division by zero exception if (1) is executed before (2)
public class Racer implements Runnable {
     int d = 42;

     public void run() {
          doSomething(1001);
          d = 0;                              // (1)
     }

     public static void main(String[] args) {
          Racer racer = new Racer();
          Thread t = new Thread(racer);
          t.start();

          doSomething(1000);
          int c = 420 / racer.d;              // (2)
          System.out.println(c);
     }
     
     static void doSomething(int n) {
          try { Thread.sleep(n); } catch (InterruptedException ix) {}
     }
}

Without any additional configuration, JPF would find and report the division by zero. If JPF is configured to verify absence of race conditions (regardless of their potential downstream effects), it will produce the following output, explaining the error and showing a counter example leading to the error
JavaPathfinder v6.0 - (C) RIACS/NASA Ames Research Center
====================================================== system under test
application: Racer.java
...
====================================================== error #1
gov.nasa.jpf.listener.PreciseRaceDetector
race for field Racer@13d.d
  main at Racer.main(Racer.java:16)
		"int c = 420 / racer.d;               "  : getfield
  Thread-0 at Racer.run(Racer.java:7)
		"d = 0;                               "  : putfield

====================================================== trace #1
---- transition #0 thread: 0
...
---- transition #3 thread: 1
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet[id="sleep",isCascaded:false,{main,>Thread-0}]
      [3 insn w/o sources]
  Racer.java:22                  : try { Thread.sleep(n); } catch (InterruptedException ix) {}
  Racer.java:23                  : }
  Racer.java:7                   : d = 0;                      
...
---- transition #5 thread: 0
gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet[id="sharedField",isCascaded:false,{>main,Thread-0}]
  Racer.java:16                  : int c = 420 / racer.d;

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 (e.g. temporal properties)
 peer classes - to execute code at the host JVM level (instead of JPF), which is mostly used to implement native methods
 bytecode factories - to provide alternative execution semantics of bytecode instructions (e.g. to implement symbolic execution)
 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

See also 
MoonWalker - similar to Java PathFinder, but for .NET programs instead of Java programs

External links 
 New NASA Software Detects 'Bugs' in Java Computer Code
 NASA Develops New Software to Detect "Bugs" in Java Computer Code

References 
 Willem Visser, Corina S. Păsăreanu, Sarfraz Khurshid. Test Input Generation with Java PathFinder. In: George S. Avrunin, Gregg Rothermel (Eds.): Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis 2004. ACM Press, 2004. .
Free software testing tools
 Willem Visser, Klaus Havelund, Guillaume Brat, Seungjoon Park, Flavio Lerda, Model Checking Programs, Automated Software Engineering 10(2), 2003.
 Klaus Havelund, Willem Visser, Program Model Checking as a New Trend, STTT 4(1), 2002.
 Klaus Havelund, Thomas Pressburger, Model Checking Java Programs using Java PathFinder, STTT 2(4), 2000.

Articles with example Java code
Software using the Apache license