The Java Pathfinder Team

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

Technologies
android, java, distributed systems, jvm
Topics
model checking, symbolic execution, program analysis, test input generation, formal methods
JPF is a highly extensible Java virtual machine built for software verification

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 2018 includes researchers from NASA Ames Research Center, Fujitsu Laboratories of America, Royal Institute of Technology - Sweden, Carnegie Mellon University , University of Minnesota, Stellenbosch University - ZA, Charles University - CZ, Teesside University - UK, University of Nebraska–Lincoln.

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, there exists many different extensions of JPF that capture different functionalities, including verification, testing, debugging, program repair and security analysis.

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.

2018 Program

Successful Projects

Contributor
Gayan Weerakutti
Mentor
Joshua Garcia, Alexander Kohan, Cyrille Artho
Organization
The Java Pathfinder Team
Support Java 9 for JPF-CORE
JPF-CORE currently builds and runs on Java 8. The main objective of this project is to get it up and running with Java 9, leveraging its new features...
Contributor
Guolong Zheng
Mentor
THANHVU NGUYEN, Quang Loc Le, Quoc-Sang Phan
Organization
The Java Pathfinder Team
Synthesis to repair heap-manipulating programs using Java StarFinder
The state of art of program repair for heap manipulating program has focus on specific properties of bugs, like null pointer dereference. We try to...
Contributor
Jeanderson Candido
Mentor
Willem Visser, Cyrille Artho
Organization
The Java Pathfinder Team
Modernizing the Java PathFinder Build Workflow: Migrating from Ant to Gradle
Developers often perform recurrent tasks during the development process such as testing, managing external libraries, generating API documentation,...
Contributor
Soha Hussein
Mentor
Willem Visser, Michael Whalen
Organization
The Java Pathfinder Team
Extending Veritesting In SPF
Veritesting, [1] is a promising technique that speeds up dynamic symbolic execution by multiple of factors [2]. In veritesting, expensive forking is...