NASA Ames Research Center

Java PathFinder

Categories:	Code analysis - Standards verifiers
Latest version:	1.0
Description:	System to verify executable Java bytecode programs. In its basic form, Java PathFinder (JPF) is a Java Virtual Machine (JVM) that is used as an explicit state software model checker, systematically exploring all potential execution paths of a program to find violations of properties like deadlocks or unhandled exceptions. Other than traditional debuggers, JPF reports the whole execution path that leads to a defect. JPF is especially suitable to find hard-to-test concurrency defects in multithreaded programs. JPF is a pure Java application that can be run either as a standalone command line tool, or embedded into systems like development environments. It was mostly developed - and is still used - at the NASA Ames Research Center. Started in 1999 as a feasibility study for software model checking, JPF since then has found its way into academia and industry, and even helped to detect defects in real spacecraft.
Added:	2005-05-04
Attributes:	[BuiltForJava] [FreeVersionAvailable] [SourceCodeProvided]