Java Pathfinder Team

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

Technologies
android, java, distributed systems, jvm
Topics
testing, verification, model checking, program analysis, environment generation
JPF is a highly extensible Java virtual machine built for sofware 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 2016 includes researchers from NASA Ames Research Center, NASA Langley Research Center, 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.

2016 Program

Successful Projects

Contributor
Blaine
Mentor
Willem Visser
Organization
Java Pathfinder Team
Fingerprinting for Programs
Fingerprinting for Programs is aimed at analyzing code blocks on a semantic level. This is done by symbolically executing the code block via SPF over...
Contributor
Jianfeng.Chen
Mentor
Franco Raimondi, neharungta, Eric Mercer
Organization
Java Pathfinder Team
Verifying Safety of NextGen Models
The goal of NASA’s NextGen research is to accommodate the traffic increase coming over the 15 years. One requirement for NextGen is to provide a...
Contributor
mmuesly
Mentor
Zvonimir, Falk Howar, Teme
Organization
Java Pathfinder Team
PSYCO for Reactive Systems
My projekt goal is to extend PSYCO by a symbolic search algorithm to generate a termination criteria for the learning phase and to enable PSYCO to...
Contributor
Octarine
Mentor
Cyrille Artho, Oksana Tkachuk
Organization
Java Pathfinder Team
Java PathFinder for Android Devices
Java PathFinder (JPF) has potential to be used for verification of Android apps, as they are written in Java. There is already an ongoing project to...
Contributor
Gunel Jahangirova
Mentor
Willem Visser, Oksana Tkachuk
Organization
Java Pathfinder Team
Oracle-Based Program Repair
The main idea of the project is to define program repairs, which make the program closest to its oracle. Initially, we have a program, which is...
Contributor
JaneOL
Mentor
Franco Raimondi, neharungta, Eric Mercer
Organization
Java Pathfinder Team
Using JPF to efficiently compute workload in Multi-Agent Systems
No one likes to arrive at the airport only to realize that their flight has been delayed. Departure Sensitive Arrival Spacing (DSAS) is a new concept...
Contributor
Chao
Mentor
Zvonimir, Falk Howar, Luckow
Organization
Java Pathfinder Team
Visualization Support for JDart
JDart is a tool for performing concolic execution on a Java program. The aim of concolic execution is to explore additional behavior in the program...
Contributor
Soothsilver
Mentor
Pavel Parizek
Organization
Java Pathfinder Team
Improving JPF Inspector
This project will bring the JPF Inspector debugging tool up to date with the most recent version of JPF and Java, and it will add additional...
Contributor
afromherz
Mentor
Corina, Luckow
Organization
Java Pathfinder Team
Extending SPF with handling of symbolic arrays, and implementing a replay module
Symbolic Pathfinder (SPF) is an open-source symbolic execution tool, based on NASA Java Pathfinder (JPF) model checker, which is used in research and...
Contributor
Jayton
Mentor
franck, Nastaran, Cyrille Artho
Organization
Java Pathfinder Team
Cache layer for jpf-nhandler
JPF is the most popular model checking tool for Java applications. It is extensible and there are lots of extensions for various purposes....