Home Page![](http://s9.addthis.com/button1-addthis.gif)
Categories: Code analysis - Standards verifiers
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 Built for Java](https://z.javatoolbox.com/style/Java.png) Built for Java |
![Free or free version available Free or free version available](https://z.javatoolbox.com/style/Free.png) Free or free version available |
![Source code provided Source code provided](https://z.javatoolbox.com/style/Source.png) Source code provided |