Skip to content

GSoC 2022 Project Ideas

Yannic Noller edited this page Feb 26, 2022 · 11 revisions

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 2022.

JPF Infrastructure

Symbolic Pathfinder (SPF)

Environment and Test Case Generation

Project Description

Support Java 11 (bootstrap methods and other issues) for jpf-core

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
Scope: 350 hours
Required skills: Knowledge of Java bytecode
Preferred skills: Knowledge of bootstrap methods in Java bytecode
Possible Mentors: Cyrille

Support for Java 12 (private API dependencies) for jpf-core

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
Scope: 175 hours
Required skills: Knowledge of Java internals
Possible Mentors: Cyrille

Test Case Generation/Model-based Testing with Modbat for JPF

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

Support for gradle for SPF

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
Scope: 175 hours
Required skills: Knowledge of Java Pathfinder and Gradle build automation
Preferred skills: Knowledge of Symbolic Pathfinder
Possible Mentors: Yannic, Corina

Support for Java v11 for SPF

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

Robustify String solving for SPF

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: Yannic, Corina, Elena, Soha

Clone this wiki locally