The Java Pathfinder Team
JPF is a highly extensible Java virtual machine built for software analysis
The Java Pathfinder project (JPF) was initially conceived and developed at NASA Ames Research Center in 1999. JPF was open sourced in April 2005 as one of the first ongoing NASA development projects to date, and it is now released under the Apache license, 2.0. JPF is a highly extensible Java virtual machine written in Java itself. It is used to create a variety of verification tools ranging from concurrency software model checkers to test case generators using symbolic execution. JPF is a research platform and a production tool at the same time. Although JPF has major contributions from companies and government agencies, our main user community is academic - there are ongoing collaborations with more than 20 universities worldwide. The JPF team for GSoC 2017 includes researchers from NASA Ames Research Center, Amazon Web Services, University of Texas at Austin, University of Texas at Dallas, Brigham Young University and the universities of London UK, Toronto CA, Tokyo JP, Basel CH, São Paulo BR, and Prague CZ.
JPF is designed to be extensible. There are well-defined extension mechanisms, directory structures and build procedures, which keep the core relatively stable and provide suitable, well separated testbeds for new ideas and alternative implementations. As a consequence we host a number of such extension projects on our own, public JPF server, together with a Wiki that provides a central location for learning about, obtaining, and contributing to JPF.
JPF has been used for a variety of application domains and research topics such as verification of multi-threaded applications, graphical user interfaces, networking, and distributed applications. In addition to its continued presence in academia, JPF has matured enough to support verification of production code and frameworks such as Android. JPF is constantly being extended with support for verification of new types of properties and for new types of application domains.
The Java Pathfinder Team 2017 Projects
Increasing SPF Performance with Bounded Static Symbolic ExecutionImproving the performance of symbolic execution to make it scale to industrial-sized programs is an important current issue. Veritesting provides a...
Java StarFinder: Symbolic Execution with Separation Logic for Testing and Verifying Heap-manipulating Programs.Symbolic PathFinder (SPF) has been very successful in testing and verifying Java bytecode programs with numeric inputs. However, its capability is...
jpf-nasExtending jpf-nas tool.
Optimize GREEN’s caching for satisfiability and model counting when using SPFMany symbolic program analysis techniques use satisfiability modulo theory (SMT) solvers to verify properties of programs. SMT solvers can provide...
Program Repair via Symbolic Execution-Derived Constraint CharacterizationThe Symbolic Execution (SPF) extension for NASA’s Java Pathfinder (JPF) has been used to generate quality test cases by symbolically executing code...
Verification and Testing of Heap-based Programs with Symbolic PathFinderSymbolic Pathfinder (SPF) is an open-source symbolic execution tool, based on the NASA Java Pathfinder (JPF) model checker, which is used in research...
Visualization of Execution TracesMultithreaded programming is becoming a mainstream programming practice, while multithreaded programming is difficult and error prone....