GSoC 2024 Project Ideas
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 2024.
Description: jpf-core is essentially a JVM that currently fully supports only Java 8 and Java 11 (with limitations on bootstrap methods). Bootstrap methods are currently interpreted, which works for common usage but may not work for advanced cases. The goal of this project is to generate the call site code on the fly so bootstrap methods work as on the host JVM.
Note: You can apply to both projects (Java 11 or 17 support); in that case, please indicate that you would like to work on either one, and what your preference would be.
Difficulty: Hard
Scope: 350 hours
Required skills: Knowledge of Java bytecode
Preferred skills: Knowledge of bootstrap methods in Java bytecode
Possible Mentors: Cyrille
Related to the project above, there are also some internal APIs from Java 11 that no longer exist in Java 17. 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 17. The code in question is easily found by trying to compile JPF with Java 17. Note: You can apply to both projects (Java 11 or 17 support); in that case, please indicate that you would like to work on either one, and what your preference would be.
Difficulty: Medium
Scope: 175 hours
Required skills: Knowledge of Java internals
Possible Mentors: Cyrille
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
Scope: 350 hours
Required skills: Knowledge of Java Pathfinder
Preferred skills: Knowledge of test generation
Possible Mentors: Cyrille
Description: The goal of this project is to upgrade SPF to work with Java 11.
Difficulty: Hard
Scope: 350 hours
Required skills: Knowledge of Symbolic Pathfinder
Preferred skills: Knowledge of Java v11
Possible Mentors: Yannic, Corina
Description: The goal of this project is to test SPF integration with Z3 string constraint solving; adding support cvc5 is a plus.
Difficulty: Hard
Scope: 350 hours
Required skills: Knowledge of Symbolic Pathfinder
Preferred skills: Knowledge of String constraint solving.
Possible Mentors: Corina, Elena, Soha
Description: The goal of this project is to support witness generation for SPF in a state-machine format based on GraphML. This would, in particular, help verify SPF's results in SV-COMP.
Difficulty: Hard
Scope: 350 hours
Required skills: Knowledge of Symbolic Pathfinder
Preferred skills: GraphML
Possible Mentors: Soha