Programming languages
JPF is a Java VM used to verify and debug software
2 projects
JPF currently cannot fully analyze Java 17 programs that use sealed classes and records — two features now standard in modern Java. This project...
Java-Ranger is a path merging extension of Symbolic Pathfinder, that collapses multiple execution paths into a single region with a disjunctive...
3 projects
Java Path Finder (JPF), a specialized Java Virtual Machine for software verification, excels with Java 8 but faces challenges with modern features in...
Java PathFinder (JPF) is an extensible software analysis framework for java bytecode which can be used to check for concurrency defects like...
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....
3 projects
This proposal aims to enhance Java Path Finder (JPF) to seamlessly support Java 17, ensuring compatibility with the latest Java version. The project...
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...
Modbat is a model-based testing framework that utilizes finite state machines (FSMs) to generate tests systematically, exploring various execution...
2 projects
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...
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...
2 projects
String solving is an important feature of symbolic execution for successful security and correctness analysis. In Java Symbolic Pathfinder (SPF), a...
Gradle is a build automation tool known for its flexibility to build software. A build automation tool is used to automate the creation of...
3 projects
To reason about string manipulating Java programs Symbolic Pathfinder (SPF) employs string constraint solvers. Currently, SPF integrates a limited...
Security and Semantic bugs exist in software systems, and discovering them is time-consuming, complicated, and challenging. Several static and...
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...
6 projects
Path merging is a promising technique that speeds up dynamic symbolic execution by multiple factors. In Path merging expensive forking is minimized...
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...
Automated Program Repair (APR) has been showing a high capability recently of fixing software bugs automatically. Despite the recent advancements,...
SPF’s constraint interface needs to be restructured. The current implementation doesn’t allow for the easy addition of new solvers and could be...
JPF does not yet fully implement the features of Java 11 - support extends only to Java 8 - including features as simple as string concatenation....
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...
6 projects
[Nakade et al. 2018] proposed to model check Habanero programs using only one program run. This project aims to further reduce state space being...
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...
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...
Symbolic execution is a powerful analysis to systematically check assertions in programs. However, the already notorious scalability problem of...
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...
Automated program repair has been gaining ground recently with substantial efforts devoted to the area. Not only has APR had great influence on...
4 projects
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...
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...
Developers often perform recurrent tasks during the development process such as testing, managing external libraries, generating API documentation,...
Veritesting, [1] is a promising technique that speeds up dynamic symbolic execution by multiple of factors [2]. In veritesting, expensive forking is...
7 projects
Symbolic Pathfinder (SPF) is an open-source symbolic execution tool, based on the NASA Java Pathfinder (JPF) model checker, which is used in research...
The Symbolic Execution (SPF) extension for NASA’s Java Pathfinder (JPF) has been used to generate quality test cases by symbolically executing code...
Improving the performance of symbolic execution to make it scale to industrial-sized programs is an important current issue. Veritesting provides a...
Symbolic PathFinder (SPF) has been very successful in testing and verifying Java bytecode programs with numeric inputs. However, its capability is...
Many symbolic program analysis techniques use satisfiability modulo theory (SMT) solvers to verify properties of programs. SMT solvers can provide...
Multithreaded programming is becoming a mainstream programming practice, while multithreaded programming is difficult and error prone....
10 projects
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...
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...
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 (JPF) has potential to be used for verification of Android apps, as they are written in Java. There is already an ongoing project to...
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...
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...
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...
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...
Symbolic Pathfinder (SPF) is an open-source symbolic execution tool, based on NASA Java Pathfinder (JPF) model checker, which is used in research and...
JPF is the most popular model checking tool for Java applications. It is extensible and there are lots of extensions for various purposes....
