Java PathFinder
Home Page
Categories: Code analysis - Standards verifiers
Author: NASA Ames Research Center
Latest version: 1.0
Added 2005-05-04
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.
Built for Java |
Free or free version available |
Source code provided |