JPF is a highly extensible Java virtual machine built for software verification

The Java Pathfinder (JPF) project 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 an extensible Java virtual machine written in Java itself. It is used to create a variety of verification and debugging tools, ranging from 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 2020 includes researchers from NASA Ames Research Center, KTH Royal Institute of Technology - Sweden, York University - Canada, Brigham Young University, Carnegie Mellon University, University of Minnesota, Humboldt University - Germany, and Charles University - Czech Republic.

JPF is designed to be highly 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 correctness properties and for new types of application domains.

lightbulb_outline View ideas list

Technologies

  • javajava
  • jvm
  • android
  • distributed systems

Topics

email Mailing list

The Java Pathfinder Team 2020 Projects

  • Carson Smith
    A Restructuring of the Path Constraint Interface
    SPF’s constraint interface needs to be restructured. The current implementation doesn’t allow for the easy addition of new solvers and could be...
  • Soha Hussein
    Extending Path Merging for SPF
    Path merging is a promising technique that speeds up dynamic symbolic execution by multiple factors. In Path merging expensive forking is minimized...
  • Quang-Cuong Bui
    LyFix: Regression Error Repair for Java Program
    Automated Program Repair (APR) has been showing a high capability recently of fixing software bugs automatically. Despite the recent advancements,...
  • Yuvaraj Anbarasan
    Support Java 11 for jpf-core
    JPF is a model checking tool for Java applications. It is a Virtual Machine (VM) for Java bytecode which executes the system under test (SUT). The...
  • Amgad Rady
    Support Java 11/12 for jpf-core
    JPF does not yet fully implement the features of Java 11 - support extends only to Java 8 - including features as simple as string concatenation....
  • Usman
    Symbolic PathFinder for Neural Network Analysis
    Symbolic PathFinder (SPF) is a tool that uses Java PathFinder at the back-end and can extract path conditions for a program by executing the program...
close

2020