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.

lightbulb_outline View ideas list


  • java
  • jvm
  • android
  • distributed systems


comment IRC Channel
email Mailing list
mail_outline Contact email

The Java Pathfinder Team 2017 Projects

  • Vaibhav B Sharma
    Increasing SPF Performance with Bounded Static Symbolic Execution
    Improving the performance of symbolic execution to make it scale to industrial-sized programs is an important current issue. Veritesting provides a...
  • Pham Hong Long
    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...
  • Jayton
    Extending jpf-nas tool.
  • Jan Taljaard
    Optimize GREEN’s caching for satisfiability and model counting when using SPF
    Many symbolic program analysis techniques use satisfiability modulo theory (SMT) solvers to verify properties of programs. SMT solvers can provide...
  • Andrew Hill
    Program Repair via Symbolic Execution-Derived Constraint Characterization
    The Symbolic Execution (SPF) extension for NASA’s Java Pathfinder (JPF) has been used to generate quality test cases by symbolically executing code...
  • Nicolas Jeannerod
    Verification and Testing of Heap-based Programs with Symbolic PathFinder
    Symbolic Pathfinder (SPF) is an open-source symbolic execution tool, based on the NASA Java Pathfinder (JPF) model checker, which is used in research...
  • Qiyi Tang
    Visualization of Execution Traces
    Multithreaded programming is becoming a mainstream programming practice, while multithreaded programming is difficult and error prone....