Java Pathfinder

Java PathFinder (JPF) is a customisable execution environment for verifying Java bytecode programs, originally developed at the NASA Ames Research Center. Its core is a Java virtual machine that explores all execution paths of a program, for example all thread interleavings, to detect defects such as deadlocks and unhandled exceptions.

JPF is extensible: projects such as symbolic execution (jpf-symbc) add test generation. It is open source and maintained on GitHub; the former NASA site no longer exists.