# Java Pathfinder

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Java_Pathfinder
> Markdown URL: https://mediated.wiki/source/Java_Pathfinder.md
> Source: https://en.wikipedia.org/wiki/Java_Pathfinder
> Source revision: 1273495213
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

Java Pathfinder Developer NASA Stable release 6.0 / November 30, 2010 (2010-11-30) Written in Java Operating system Cross-platform Size 1.6 MB (archived) Type Software verification tool, Virtual machine License Apache License Version 2 Website https://github.com/javapathfinder/

**Java Pathfinder** (JPF) is a system to verify executable [Java bytecode](/source/Java_bytecode) programs. JPF was developed at the [NASA](/source/NASA) [Ames Research Center](/source/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](/source/Java_Virtual_Machine). JPF executes normal [Java bytecode](/source/Java_bytecode) programs and can store, match and restore program states. Its primary application has been [Model checking](/source/Model_checking) of [concurrent programs](/source/Concurrent_computing), to find defects such as [data races](/source/Race_condition) and [deadlocks](/source/Deadlock_(computer_science)). 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.

## 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](/source/Java_Native_Interface). 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](/source/Combinatorial_explosion), although it performs on-the-fly [Partial order reduction](/source/Partial_order_reduction)

- the configuration system for JPF modules and runtime options can be complex

## See also

- [MoonWalker](http://fmt.cs.utwente.nl/tools/moonwalker/) - similar to Java PathFinder, but for .NET programs instead of Java programs

## External links

- [New NASA Software Detects 'Bugs' in Java Computer Code](https://www.nasa.gov/centers/ames/news/releases/2005/05_28AR.html)

- [NASA Develops New Software to Detect "Bugs" in Java Computer Code](https://www.nasa.gov/centers/ames/multimedia/images/2005/javapathfinder.html)

## References

- Willem Visser, [Corina S. Păsăreanu](/source/Corina_P%C4%83s%C4%83reanu), Sarfraz Khurshid. [Test Input Generation with Java PathFinder.](http://users.ece.utexas.edu/~khurshid/papers/JPF-issta04.pdf) In: George S. Avrunin, Gregg Rothermel (Eds.): Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis 2004. ACM Press, 2004. [ISBN](/source/ISBN_(identifier)) [1-58113-820-2](https://en.wikipedia.org/wiki/Special:BookSources/1-58113-820-2).

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

---
Adapted from the Wikipedia article [Java Pathfinder](https://en.wikipedia.org/wiki/Java_Pathfinder) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Java_Pathfinder?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.