We are hiring new student research assistants and tutors. Apply now!
4 papers accepted at SPIN 2024!

Google Summer of Code 2024

Ideas

Below you can find a list of selected project ideas for GSoC, categorized according to our main development projects. If you are searching for more topics or want to propose your own, there is a list with more ideas available. You can also take a look into the tickets for the specific projects on the corresponding repository websites. The assigned mentors listed below are not fixed yet and might be changed.
If you have any questions, please contact us!

CPAchecker (website)

CPAchecker is an award-winning open-source framework for software verification. It is written in Java and based on a highly modular architecture that allows to develop and combine a wide range of different analyses. CPAchecker is used for verification of the Linux kernel and has helped to find hundreds of bugs in the kernel.

Infrastructure for Software Verification

Automated software verifiers are powerful tools to find bugs in programs, but they are often complex and difficult to use. Our team aims to simplify this and make it easy to integrate software verifiers into the software-development process.

CPA-Daemon is a gRPC-based microservice that enables users to run the award-winning verifier CPAchecker in a cloud setup. It focuses on ease of use and continuous verification. In the scope of GSoC, we want to improve the infrastructure surrounding CPA-Daemon. We offer the following project:

Btor2-Cert (website)

Btor2-Cert is a certifying and validating hardware-verification framework using software analyzers. It translates a word-level hardware circuit in the Btor2 format to a behaviorally equivalent C program using Btor2C, verify the C program with a certifying software analyzer, translate the witness (i.e., certificate) produced by the analyzer back to the Btor2 domain, and validate the witness with Btor2-Val. Btor2-Cert offers a convenient way to integrate different backend software analyzers and provides trustworthy verification results accompanied by inspectable witnesses, making it a flexible and powerful framework for hardware verification.

JavaSMT (website)

JavaSMT is a common API layer for accessing various SMT solvers. It was created out of our experience integrating and using different SMT solvers in the CPAchecker project. JavaSMT can express formulas in the theory of integers, rationals, bitvectors, floating-points, and uninterpreted-functions, and supports model generation, interpolation, formula inspection and transformation.

PJBDD (website)

PJBDD is a multi-threaded Binary Decision Diagram (BDD) library written in Java. It supports concurrent computation as well as parallel operations and automated resource management. BDDs are compact representation for Boolean formulas and can be used for efficient manipulation.

BenchExec (website)

BenchExec is a benchmarking framework for Linux (written in Python) that is aimed at a high reliability of the results. It can measure the CPU-time and peak memory usage of whole groups of processes. To do so, it makes use of modern Linux features such as cgroups and namespaces, effectively creating a benchmarking container whose resource usage is measured. The concepts and architecture of BenchExec are described in a paper (open access).

Instructions for Contributors

Prospective contributors wishing to participate in Google Summer of Code must realize that this is an important professional opportunity. You will contribute code for an award-winning tool chain or parts of its infrastructure. Therefore, we seek contributors who are committed to helping our tools long-term and are willing to both do quality work, and be proactive in communication with their mentors.

You don't have to be a proven developer - in fact, this whole program is meant to facilitate joining our group and take a look at open source communities. However, experience in coding is welcome and should be mentioned in your proposal.

You should take a look at the tools that you plan to work on before the start date. The timeline from Google reserves a lot of time for bonding periods; use that time wisely. Good communication is important. The group members are available via mail (or online/in-person meeting, if needed). You should communicate with your mentor, and formally report progress and plans weekly.

Recommended steps

Contributor Proposal Guidelines

Proposals are the basis of the GSoC projects. Write a clear proposal on what you plan to do, the scope of your work, and why we should choose you to do it. The proposals are the basis of our decisions of which contributor to choose.

Contributors can use the following application template:

Accepted Contributors

Your primary responsibility is finishing your project under the guidance of your mentors. To do that, you must submit code regularly and stay in frequent communication with your mentor and our team. For the evaluation, you must succeed with communication, coding, and documentation.

Hints

Google Summer of Code in Previous Years

To get information about former projects and ideas, you can take a look at the pages from previous years: