Software and Computational Systems Lab

Google Summer of Code 2023

Contributors

Bastiaan Laarakker, University of Amsterdam

• Topic: Implementing backward bounded model checking in CPAchecker
• Mentor: Nian-Ze Lee
• Code:
  1. Supporting witness export for backward analysis
  2. Implementation of backward BMC algorithm
  3. Pointer aliasing for backward analysis
• Final report

George Granberry, Chalmers University of Technology

• Topic: Scaling Formal Verification
• Mentor: Matthias Kettl
• Code: GitLab MR
• Final report

Jia Sun, Kyoto University

• Topic: Reverse Program Synthesis for Backward Reachability Analysis
• Mentor: Po-Chun Chien
• Code: GitLab MR
• Final report

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.

• Scaling Formal Verification: Parallel Analysis of Functions

  Verifying complex programs with respect to a given specification (e.g., check that function reach_error is never called) may be time consuming. To make verifiers more applicable in industry, we want to tackle the problem with a divide-and-conquer approach. We decompose the verification task into multiple smaller tasks that are then verified in parallel. As soon as one of the analyses finds a violation, we abort all other analyses and report the violation. This might lead to many false alarms since we do not know with which input parameters functions are called. As a first step, return values of functions are ignored and interpreted as unknown value. From there we can continue in two directions:

  1. Analyze functions under a user-defined condition (e.g., a user restricts the values of parameter x of function foo to the interval [0:100])
  2. Identify each function call automatically and try to infer all parameters.
  The goals of this topic are:
  1. The verification verdict should be available faster (in terms of elapsed walltime).
  2. Wrong proofs should not exist. In case a program is safe, the decomposition should be a sound over-approximation.
  Finally, we will evaluate this approach on the SV-COMP benchmark set. This topic is inspired by the tool Infer.

  Requirements: Programming in Java, reading C code

  Mentor: Matthias Kettl

• Implement Dual Approximated Reachability Algorithm

  Dual Approximated Reachability (DAR) is an interpolation-based verification algorithm that combines forward and backward reachability analysis. The goal is to have this algorithm implemented in CPAchecker and evaluate it against other verification approaches over the SV-COMP benchmark set.

  Requirements:

  • Ability to program in Java
  • Basic knowledge of SAT/SMT solving, Craig's interpolation, and model checking

  Mentor: Nian-Ze Lee, Po-Chun Chien

• Reverse Program Synthesis for Backward Reachability Analysis

  In most verification tools, the reachability analysis searches for a path from the initial program location to the error location. The analysis could also be done backward, i.e. tries to reach the initial location from the error location. The goal of this project is to implement a control-flow automata (CFA) transformer in CPAchecker that reverses program executions by following the transitions backward, such that for any program path in the original CFA, there is a corresponding equisatisfiable path in the reverse CFA. After the transformation, one could then apply existing analysis to verify the reverse CFA.

  Requirements:

  • Ability to program in Java and understand C code
  • Basic knowledge of control-flow automata

  Mentor: Nian-Ze Lee, Po-Chun Chien

• Implement Backward Symbolic Execution

  Symbolic execution is a well-known software analysis technique that searches for execution paths that could lead to the error location from the initial program location. Backward symbolic execution, on the contrary, follows the execution backward and searches paths from the error location to the initial location. The goal of the project is to implement such technique in CPAchecker.

  Requirements:

  • Ability to program in Java and understand C code
  • Basic knowledge of SAT/SMT solving and weakest precondition

  Mentor: Nian-Ze Lee, Po-Chun Chien

• Implement Single-Loop Transformation

  Single-loop transformation is a process that converts a program with an arbitrary loop structure (, which may contain nested and/or multiple loops) to an equivalent program with only one loop. Though such transformation already exists in CPAchecker, we would like to re-implement it with the new control-flow automata transformer, which provides more useful features and functionalities.

  Requirements:

  • Ability to program in Java and understand C code
  • Basic knowledge of control-flow automata and compiler (esp. loop rewriting)

  Mentor: Nian-Ze Lee, Po-Chun Chien

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.

• Integrate more SMT solvers

  There are plenty of SMT solvers that can be integrated into our library. This project aims to integrate several of them and provide bindings via the Java Native Interface. We would also like to have an automated build process, integration tests, documentation, etc. A possible candidate is dReal or other projects focused on SMT solving.

  Requirements: Java, C/C++ (depending on the integrated solver)

  Mentor: Daniel Baier

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.

• Extend the library with more decision diagrams

  PJBDD already supports BDDs, Chained BDDs, Tagged BDDs and Zero Suppressed BDDs (ZDDs), but there are more different types of decision diagrams (DDs) such as Chained ZDDs or Algebraic Decision Diagrams (ADDs). Depending on the Boolean formula, different graph based representations may significantly vary in size and construction performance. The goal of this project is to extend PJBDD with different DDs, but with one general API such that the DDs can be used replaceable.

  Requirements: Java

  Mentor: Daniel Baier

• Optimization with reduction rules

  There are various optimization techniques that can be applied to decision diagrams. One such example would be BDDs with complemented edges and edge-specified reductionss (CESRBDDs), which enables a BDD to be reduced even more than already implenented techniques such as tagged or zero-suppressed BDDs , while remaining a compact form. The goal of this project is to incorporate these techniques in PJBDD and perform evaluation with a case study.

  Requirements: Java

  Mentor: Daniel Baier

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

• Modern Tests

  BenchExec's tests are currently written using the test framework nose, which is not maintained anymore and has problems on new Python versions. The goal of this project is to switch the test framework used for BenchExec. As a first step, an appropriate framework needs to be chosen. This should be done systematically based on criteria like ease of use, how common the framework is, whether it is well maintained etc. Next, the framework needs to be integrated in BenchExec's project structure and the existing tests need to adjusted where necessary. This might also include restructuring the tests and in general improving their state. Filling gaps in our test coverage with more unit tests would also be highly welcome. (Cf. corresponding GitHub issue with more information)

  Requirements: Python

  Mentor: Philipp Wendler

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

• Read Google's instructions for participating and the GSoC Contributor Manual.
• Take a look at the list of ideas.
• Get familiar with the project you are interested in, e.g., by trying it out, reading the documentation, etc. If you already see something that can be improved, file a pull request!
• Contact the developers of the project of your choice, e.g., via the mailing list or the mentor, introduce yourself, and meet your fellow developers.
• Come up with a topic for a GSoC project that you're interested in.
• Write a first draft proposal and get someone to review it.
• Submit your proposal using Google's web interface ahead of the deadline.

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:

• Introduction and Background: You can either choose a problem from the list of ideas or state a new problem for our group. Before offering the solution (your GSoC project), you should first define the problem. What is the current state of things? What is the issue you wish to solve and why? What is your solution?
• Project Goals: Propose a clear list of deliverables, explaining exactly what you promise to do and what you do not plan to do.
• Implementation: Describe what you plan to do as a solution for the problem you defined above. Include technical details, showing that you understand the technology.
• Timeline: Show that you understand the problem and have a solution. Divide the solution into manageable parts (estimated work items, milestones) and describe a detailed realistic plan on how to accomplish your goal. Include time for searching and fixing bugs, and communication. Do not promise what you cannot keep.
  Other commitments during GSoC, such as a job, vacation, and exams should also be mentioned. GSoC should be treated like a full-time job, and we will expect approximately 30 hours of work per week. Explain how you will work around conflicts.
  Describe your plans for communication. You will need to participate on weekly communication such as detailed email or personal meeting with your mentor or the team.
• About Me: Provide your contact information (address, email, phone) and write a few sentences about you and why you think you are the best for this job. Previous contributions to our projects are appreciated. Name people (other developers, students, professors) who can act as a reference for you. Mention your field of study if necessary.
  Tell us if you are submitting proposals to other organizations, and whether or not you would choose our group if given the choice.
  If your native language is not German or English, you should be able to communicate in one of those languages.

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

• Submit your proposal early! Early submissions will be read and discussed by mentors more eagerly.
• Keep it simple! Be concise and precise. Provide a clear, descriptive title.
• Know what you are talking about! Do not submit ideas that cannot be accomplished realistically or that are not related to our projects.
• Aim wide! You can submit more than one proposal, with different ideas. If you do submit more than one proposal, tell us which of them you would prefer, if more were selected.

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:

• GSoC 2019 webpage and GSoC 2019 project site
• GSoC 2018 webpage and GSoC 2018 project site