Java Pathfinder

<h2 id="extensibility">Extensibility</h2>
<p>JPF is an open system that can be extended in a variety of ways. The main extension constructs are
</p>
<ul><li><i>listeners</i> -  to implement complex properties (e.g. temporal properties)</li>
<li><i>peer classes</i> - to execute code at the host JVM level (instead of JPF), which is mostly used to implement native methods</li>
<li><i>bytecode factories</i> - to provide alternative execution semantics of bytecode instructions (e.g. to implement symbolic execution)</li>
<li><i>choice generators</i> - to implement state space branches such as scheduling choices or data value sets</li>
<li><i>serializers</i> - to implement program state abstractions</li>
<li><i>publishers</i> - to produce different output formats</li>
<li><i>search policies</i> - to use different program state space traversal algorithms</li></ul>
<p>JPF includes a runtime module system to package such constructs into separate <i>JPF extension projects</i>. 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.
</p>
<h2 id="limitations">Limitations</h2>
<ul><li>JPF cannot analyze <a href="/facts/Java_Native_Interface/Q3E0I6lL">Java native methods</a>. If the system under test calls such methods, these have to be provided within peer classes, or intercepted by listeners</li>
<li>as a model checker, JPF is susceptible to <a href="/facts/Combinatorial_explosion/TN8pUrtI">Combinatorial explosion</a>, although it performs on-the-fly <a href="/facts/Partial_order_reduction/SHkcqWzV">Partial order reduction</a></li>
<li>the configuration system for JPF modules and runtime options can be complex</li></ul>
<h2 id="see-also">See also</h2>
<ul><li><a href="http://fmt.cs.utwente.nl/tools/moonwalker/">MoonWalker</a> - similar to Java PathFinder, but for .NET programs instead of Java programs</li></ul>
<h2 id="external-links">External links</h2>
<ul><li><a href="https://www.nasa.gov/centers/ames/news/releases/2005/05_28AR.html">New NASA Software Detects 'Bugs' in Java Computer Code</a></li>
<li><a href="https://www.nasa.gov/centers/ames/multimedia/images/2005/javapathfinder.html">NASA Develops New Software to Detect "Bugs" in Java Computer Code</a></li></ul>

<ul><li>Willem Visser, <a href="/facts/Corina_P%25C4%2583s%25C4%2583reanu/5fwVzE7q">Corina S. Păsăreanu</a>, Sarfraz Khurshid. <a href="http://users.ece.utexas.edu/~khurshid/papers/JPF-issta04.pdf">Test Input Generation with Java PathFinder.</a> In: George S. Avrunin, Gregg Rothermel (Eds.): Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis 2004. ACM Press, 2004. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 1-58113-820-2.</li>
<li>Willem Visser, Klaus Havelund, Guillaume Brat, Seungjoon Park, Flavio Lerda, Model Checking Programs, Automated Software Engineering 10(2), 2003.</li>
<li>Klaus Havelund, Willem Visser, Program Model Checking as a New Trend, STTT 4(1), 2002.</li>
<li>Klaus Havelund, Thomas Pressburger, Model Checking Java Programs using Java PathFinder, STTT 2(4), 2000.</li></ul>

Java Pathfinder open-in-new

Java Pathfinder