The Java Pathfinder Team

An extensible software analysis framework for Java bytecode

Technologies
android, java, distributed systems, jvm, bytecode
Topics
testing, concurrency, program analysis, virtual machine, software model checking
An extensible software analysis framework for Java bytecode

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 Labs. of America, KTH 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 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.

2019 Program

Successful Projects

Contributor
Egor Namakonov
Mentor
Eric Mercer, Pavel Parízek
Organization
The Java Pathfinder Team
Boosting data race detection by extinguishing state explosion
[Nakade et al. 2018] proposed to model check Habanero programs using only one program run. This project aims to further reduce state space being...
Contributor
Manish Thakur
Mentor
Alexander Kohan, Cyrille Artho
Organization
The Java Pathfinder Team
Parallel implementation of Java Pathfinder Project
One of the major challenges faced when applying model checking is the state space explosion, due to which it becomes impossible to detect errors in...
Contributor
Kyle Storey
Mentor
Eric Mercer, Pavel Parízek
Organization
The Java Pathfinder Team
Dynamic Partial Order Reduction Engine connected with Symbolic Data Race Detection for Habanero Java
A engine to simplify Dynamic Partial Order Reduction in JPF as well as a tool to efficiently prove or disprove data race freedom in structured...
Contributor
Junye Wen
Mentor
corinus, Yannic Noller, Guowei Yang
Organization
The Java Pathfinder Team
Checking Assertions with Symbolic Pathfinder
Symbolic execution is a powerful analysis to systematically check assertions in programs. However, the already notorious scalability problem of...
Contributor
Yuvaraj Anbarasan
Mentor
Franck van Breugel, Willem Visser, Cyrille Artho
Organization
The Java Pathfinder Team
Support gradle for jpf-core and extensions.
JPF is a model checking tool for java applications. JPF-core is the core structure of JPF. The build for jpf-core has been moved from ant (upto java...
Contributor
Hanliang Zhang
Mentor
Quoc-Sang Phan, Dinh Xuan Bach Le
Organization
The Java Pathfinder Team
NFix
Automated program repair has been gaining ground recently with substantial efforts devoted to the area. Not only has APR had great influence on...