-
Notifications
You must be signed in to change notification settings - Fork 351
GSoC 2025 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 2025.
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.
Difficulty: Hard
Scope: 350 hours
Required skills: Knowledge of Java bytecode
Preferred skills: Knowledge of private Java APIs
Possible Mentors: Cyrille
Related to the project above, there are also some new features in Java 17 that are not yet supported by JPF. We have work in progress on branch java-17
. Currently unsupported Java features include language features that are not supported at run time (e.g., records) and Java language features that are not fully analyzed (e.g., sealed classes). In this project, you would identify such unsupported features and extend JPF (jpf-core) to support them.
Difficulty: Medium
Scope: 175 hours
Required skills: Knowledge of Java internals
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
Please contact us by creating an issue. We are trying to fix the process below, which no longer works.
-
How to obtain and install JPF
- System requirements
- Downloading
- Creating a site properties file
- Building, testing, and running
- JPF plugins
-
Developer guide
- Top-level design
- Key mechanisms
- Extension mechanisms
- Common utilities
- Running JPF from within your application
- Writing JPF tests
- Coding conventions
- Hosting an Eclipse plugin update site