The JPF team

JPF is a special JVM for software verification

Technologies

android
java
distributed systems
jvm
bytecode
smt solvers

Topics

testing
verification
model checking
program analysis
environment generation
symbolic execution
test input generation
formal methods
concurrency
virtual machine
software model checking
verification of concurrent systems
jvm
https://github.com/javapathfinder/jpf-core/wiki
Chat
Email
Mailing List / Forum
Twitter

Projects

Contributor

Blaine

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...

View project detailsView code

Contributor

Jianfeng.Chen

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...

View project detailsView code

Contributor

mmuesly

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...

View project detailsView code

Contributor

Octarine

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...

View project detailsView code

Contributor

Gunel Jahangirova

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...

View project detailsView code

Contributor

JaneOL

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...

View project detailsView code

Contributor

Chao

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...

View project detailsView code

Contributor

Soothsilver

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...

View project detailsView code

Contributor

afromherz

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...

View project detailsView code

Contributor

Jayton

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....

View project detailsView code