imported>HyperAccelerated: Remove unsourced example

2025-02-02T15:58:32Z

Remove unsourced example

New page

{{Infobox Software
| name = Java Pathfinder
| logo =
| screenshot =
| caption =
| developer = [[NASA]]
| latest release version = 6.0
| latest release date = {{release date|2010|11|30}}
| operating system = [[Cross-platform]]
| size = 1.6 MB (archived)
| programming language = [[Java (programming language)|Java]]
| genre = [[Software verification]] tool, [[Virtual machine]]
| license = [[Apache License|Apache License Version 2]]
| website = https://github.com/javapathfinder/
}}

'''Java Pathfinder''' (JPF) is a system to verify executable [[Java bytecode]] programs. JPF was developed at the [[NASA]] [[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]]. JPF executes normal [[Java bytecode]] programs and can store, match and restore program states. Its primary application has been [[Model checking]] of [[Concurrent computing|concurrent programs]], to find defects such as [[Race condition|data races]] and [[Deadlock (computer science)|deadlock]]s. 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 Interface|Java native methods]]. 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]], although it performs on-the-fly [[Partial order reduction]]
* the configuration system for JPF modules and runtime options can be complex

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

== External links ==
* [https://www.nasa.gov/centers/ames/news/releases/2005/05_28AR.html New NASA Software Detects 'Bugs' in Java Computer Code]
* [https://www.nasa.gov/centers/ames/multimedia/images/2005/javapathfinder.html NASA Develops New Software to Detect "Bugs" in Java Computer Code]

== References ==
* Willem Visser, [[Corina Păsăreanu|Corina S. Păsăreanu]], Sarfraz Khurshid. [http://users.ece.utexas.edu/~khurshid/papers/JPF-issta04.pdf Test Input Generation with Java PathFinder.] In: George S. Avrunin, Gregg Rothermel (Eds.): Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis 2004. ACM Press, 2004. {{ISBN|1-58113-820-2}}.
[[Category:Free software testing tools]]
* 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.

[[Category:Articles with example Java code]]
[[Category:Software using the Apache license]]

Java Pathfinder - Revision history

imported>HyperAccelerated: Remove unsourced example