Support for Java 17 in jpf-core
Contributor: Darshan Raghavendrachari
JPF currently cannot fully analyze Java 17 programs that use sealed classes and records — two features now standard in modern Java. This project...
Programming languages
The JPF team
JPF is a Java VM used to verify and debug software
Technologies
androiddistributed systemsJavajvm
Topics
model checkingprogram analysissymbolic executiontest input generationverification of concurrent systems
- Total projects
- 48
- Years participating
- 11
- Most recent
- 2026
Participation history
Historical projects
Support Floating Point Constraints for Path-Merged Regions
Contributor: Salmane Khalili
Java-Ranger is a path merging extension of Symbolic Pathfinder, that collapses multiple execution paths into a single region with a disjunctive...
Support Java 11/17 for JPF extensions
Contributor: Mahmoud Khawaja
Java Path Finder (JPF), a specialized Java Virtual Machine for software verification, excels with Java 8 but faces challenges with modern features in...
Support portfolio of solvers in SPF
Contributor: Rehan Chalana
Java PathFinder (JPF) is an extensible software analysis framework for java bytecode which can be used to check for concurrency defects like...
Support Runtime Exception In SPF
Contributor: Saiff
The main goal of this project is to add support for handling runtime exceptions in SPF that will improve SPF's performance on SV-COMP benchmarks....
Support for Java 17 for jpf-core
Contributor: Rahul Kumar (Ekla)
This proposal aims to enhance Java Path Finder (JPF) to seamlessly support Java 17, ensuring compatibility with the latest Java version. The project...
Support the generation of violation witness in graphML format in SPF
Contributor: Kunha Kim
Our final goal of this project is to obtain missing scores for Symbolic PathFinder(SPF) in SV-COMP. There are two main reasons why SPF is losing many...
Model-based Testing with Modbat for JPF
Contributor: Harshvardhan Parmar
Modbat is a model-based testing framework that utilizes finite state machines (FSMs) to generate tests systematically, exploring various execution...
Better Java 11 Support for Java Pathfinder
Contributor: Daohan Qu
Java Pathfinder (JPF) is a Java virtual machine that can run compiled Java programs as well as model checking it. It is also an extensible software...
Support Java 11 (bootstrap methods and other issues) for jpf-core
Contributor: varad_galgali
jpf-core is essentially a JVM that currently fully supports only Java 8. The goal of this project is to make it up-to-date with new features of Java...
Support More Java String Functions in SPF
Contributor: Qiuchen Yan
String solving is an important feature of symbolic execution for successful security and correctness analysis. In Java Symbolic Pathfinder (SPF), a...
Add Gradle support for SymbolicPathFinder
Contributor: Gaurang Pramod Kudale
Gradle is a build automation tool known for its flexibility to build software. A build automation tool is used to automate the creation of...
Improved Integration of String Solvers in SPF
Contributor: Marlin Roberts
To reason about string manipulating Java programs Symbolic Pathfinder (SPF) employs string constraint solvers. Currently, SPF integrates a limited...
Using Lightweight Specifications with Fuzzing and Symbolic Execution to Reveal Security and Semantic Bugs
Contributor: Amirfarhad Nilizadeh
Security and Semantic bugs exist in software systems, and discovering them is time-consuming, complicated, and challenging. Several static and...
Systematically explore bit-flip faults in user-specified variables in Java programs
Contributor: Pu (Luke) Yi
Computer hardware is susceptible to errors. For example, radiation may induce error to the hardware and some bit might be flipped. It is important to...
Extending Path Merging for SPF
Contributor: Soha Hussein
Path merging is a promising technique that speeds up dynamic symbolic execution by multiple factors. In Path merging expensive forking is minimized...
Symbolic PathFinder for Neural Network Analysis
Contributor: Usman
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...
LyFix: Regression Error Repair for Java Program
Contributor: Quang-Cuong Bui
Automated Program Repair (APR) has been showing a high capability recently of fixing software bugs automatically. Despite the recent advancements,...
A Restructuring of the Path Constraint Interface
Contributor: Carson Smith
SPF’s constraint interface needs to be restructured. The current implementation doesn’t allow for the easy addition of new solvers and could be...
Support Java 11/12 for jpf-core
Contributor: Amgad Rady
JPF does not yet fully implement the features of Java 11 - support extends only to Java 8 - including features as simple as string concatenation....
Support Java 11 for jpf-core
Contributor: Yuvaraj Anbarasan
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...
Boosting data race detection by extinguishing state explosion
Contributor: Egor Namakonov
[Nakade et al. 2018] proposed to model check Habanero programs using only one program run. This project aims to further reduce state space being...
Parallel implementation of Java Pathfinder Project
Contributor: Manish Thakur
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...
Dynamic Partial Order Reduction Engine connected with Symbolic Data Race Detection for Habanero Java
Contributor: Kyle Storey
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...
Checking Assertions with Symbolic Pathfinder
Contributor: Junye Wen
Symbolic execution is a powerful analysis to systematically check assertions in programs. However, the already notorious scalability problem of...
Support gradle for jpf-core and extensions.
Contributor: Yuvaraj Anbarasan
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...
NFix
Contributor: Hanliang Zhang
Automated program repair has been gaining ground recently with substantial efforts devoted to the area. Not only has APR had great influence on...
Support Java 9 for JPF-CORE
Contributor: Gayan Weerakutti
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...
Synthesis to repair heap-manipulating programs using Java StarFinder
Contributor: Guolong Zheng
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...
Modernizing the Java PathFinder Build Workflow: Migrating from Ant to Gradle
Contributor: Jeanderson Candido
Developers often perform recurrent tasks during the development process such as testing, managing external libraries, generating API documentation,...
Extending Veritesting In SPF
Contributor: Soha Hussein
Veritesting, [1] is a promising technique that speeds up dynamic symbolic execution by multiple of factors [2]. In veritesting, expensive forking is...
Verification and Testing of Heap-based Programs with Symbolic PathFinder
Contributor: Nicolas Jeannerod
Symbolic Pathfinder (SPF) is an open-source symbolic execution tool, based on the NASA Java Pathfinder (JPF) model checker, which is used in research...
jpf-nas
Contributor: Jayton
Extending jpf-nas tool.
Program Repair via Symbolic Execution-Derived Constraint Characterization
Contributor: Andrew Hill
The Symbolic Execution (SPF) extension for NASA’s Java Pathfinder (JPF) has been used to generate quality test cases by symbolically executing code...
Increasing SPF Performance with Bounded Static Symbolic Execution
Contributor: Vaibhav B Sharma
Improving the performance of symbolic execution to make it scale to industrial-sized programs is an important current issue. Veritesting provides a...
Java StarFinder: Symbolic Execution with Separation Logic for Testing and Verifying Heap-manipulating Programs.
Contributor: Pham Hong Long
Symbolic PathFinder (SPF) has been very successful in testing and verifying Java bytecode programs with numeric inputs. However, its capability is...
Optimize GREEN’s caching for satisfiability and model counting when using SPF
Contributor: Jan Taljaard
Many symbolic program analysis techniques use satisfiability modulo theory (SMT) solvers to verify properties of programs. SMT solvers can provide...
Visualization of Execution Traces
Contributor: Qiyi Tang
Multithreaded programming is becoming a mainstream programming practice, while multithreaded programming is difficult and error prone....
Fingerprinting for Programs
Contributor: Blaine
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...
Verifying Safety of NextGen Models
Contributor: Jianfeng.Chen
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...
PSYCO for Reactive Systems
Contributor: mmuesly
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...
Java PathFinder for Android Devices
Contributor: Octarine
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...
Oracle-Based Program Repair
Contributor: Gunel Jahangirova
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...
Using JPF to efficiently compute workload in Multi-Agent Systems
Contributor: JaneOL
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...
Visualization Support for JDart
Contributor: Chao
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...
Improving JPF Inspector
Contributor: Soothsilver
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...
Extending SPF with handling of symbolic arrays, and implementing a replay module
Contributor: afromherz
Symbolic Pathfinder (SPF) is an open-source symbolic execution tool, based on NASA Java Pathfinder (JPF) model checker, which is used in research and...
Cache layer for jpf-nhandler
Contributor: Jayton
JPF is the most popular model checking tool for Java applications. It is extensible and there are lots of extensions for various purposes....