Please note that this list is not exclusive. If you have other ideas and topics related to JPF, please let us know on the JPF Google group. A possible proposal template can be found at the bottom of our GSoC page: [[JPF Google Summer of Code 2021]].
Description: 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 11. The JPF source itself has already been made compatible with Java 11. Now, JPF should support new features of Java 11 bytecode. Thanks to work in 2019 and especially 2020, a lot of this works now, but there is still work left to do.
The key feature of Java 11 that is currently not fully supported are bootstrap methods that are generated at load time. They are used for things as common as string concatenation ("Hello, " + name). As of now, many cases are supported, but there are still many programs (and unit tests) that fail with Java 11. It is therefore very important for us that we support the general case of this feature. The current state can be seen by running the unit tests of branch java-10-gradle with Java 11 and by looking at Issue #274.
This is a high-priority project, as support for Java 8 is limited to the near future. Note: You can apply to both projects (Java 11 or 12 support); in that case, please indicate that you would like to work on either one, and what your preference would be.
Difficulty: Hard
Required skills: Knowledge of Java bytecode
Preferred skills: Knowledge of bootstrap methods in Java bytecode
Related to the project above, there are also some internal APIs from Java 11 that no longer exist in Java 12 and later.
This requires redesigning and reimplementing part of the code, in order to take a different approach that no longer depends on functionality that was removed in Java 12. The code in question is easily found by trying to compile branch java-10-gradle with Java 12.
Note: You can apply to both projects (Java 11 or 12 support); in that case, please indicate that you would like to work on either one, and what your preference would be.
Difficulty: Medium
Required skills: Knowledge of Java internals
Description: JPF requires test cases as a starting point to explore a system. It is therefore suitable to use test case generation to create test cases automatically. Modbat is an open-source tool for test case generation. For testing concurrent software, an obvious choice would be to combine Modbat (to generate tests) with JPF (to execute tests and find concurrency problems). This has been done once as a proof of concept but is not supported in the current version of Modbat. The main reason for this is that Modbat's reporting has to read and parse bytecode, which requires access to some native code that JPF does not support. The goal is to find all problems where Modbat requires native access, and to use jpf-nhandler to resolve as many of these cases as possible. Remaining cases can be handled with custom model/peer classes, perhaps not with the full feature set, but at least to avoid JPF aborting due to an unsupported feature.
Difficulty: Easy
Required skills: Knowledge of Java Pathfinder
Preferred skills: Knowledge of test generation
Description: The goal of this project is to (1) implement gradle support for Symbolic Pathfinder, (2) to update the extension template, including gradle support and updated documentation.
Difficulty: Easy
Required skills: Knowledge of Java Pathfinder and Gradle build automation
Preferred skills: Knowledge of Symbolic Pathfinder
Description: Symbolic PathFinder incorporates several String constraint solvers to enable analysis of programs that process Strings. The project will evaluate the current integration of a string constraint solver into SPF and fix current integration issues with String solvers.
Difficulty: Medium
Required skills: Knowledge of symbolic execution, automata theory.
Preferred skills: Familiarity with Symbolic PathFinder, knowledge of a string constraint solver or familiarity with String decision procedures.
Description: SPF currently uses a depth-first search strategy, in this project we will add random search strategy to SPF. This will allow SPF to have faster coverage given a limited time budget.
Difficulty: Medium
Required skills: Knowledge of Symbolic Pathfinder.
Preferred skills: Knowledge of random search strategy.
Description: When generating test cases for path-merging more branch obligations could be covered with a single test case. In this project, we will focus on ways to minimize the number of test cases generated from path-merging for branch coverage criteria.
Difficulty: Medium
Required skills: Knowledge of Symbolic PathFinder.
Preferred skills: Knowledge of Java Ranger.
Using Lightweight Specifications with Fuzzing and Symbolic Execution to Reveal Security and Semantic Bugs
Description: In this work, we plan to investigate the benefits of using lightweight program specifications in conjunction with hybrid fuzzing methods to discover security and semantic bugs in Java programs. We plan to build on Badger (a guided fuzzer tool for Java using SPF) and the runtime assertion checker of OpenJML. Badger will be used to generate test inputs to achieve branch coverage. OpenJML will be used to filter invalid inputs, revealing security and semantic bugs using the lightweight specification with running valid inputs.
Difficulty: Medium
Required skills: Knowledge of Symbolic Pathfinder
Preferred skills: Knowledge of Badger and Kelinci, Fuzzing in general