Software and Computational Systems Lab

Google Summer of Code 2018

Software and Computational Systems Lab at LMU Munich has been selected as a Google Summer of Code 2018 mentor organization.

A printable poster can be downloaded here.

Ideas

This list of ideas gives an overview of projects especially for GSoC. If you are searching for more topics, there is a list with more ideas available. You can also take a look into the tickets for the specific projects. If you have any questions, please contact us. The assigned mentor are not yet fixed and might be changed.

CPAchecker (website)

CPAchecker is an award-winning open-source framework for the verification of software. 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 more than 50 bugs in the kernel.

• Eclipse plugin

  In order to make CPAchecker and verification in general more usable for software developers, it should be integrated into IDEs. The goal of this project is to develop an Eclipse plugin for CPAchecker that allows users of Eclipse CDT (the Eclipse environment for C programs) to use CPAchecker, similar to an existing Eclipse plugin for the verifier CBMC. Developers should be able to choose which program and what they would like to verify (e.g., checking all assert statements or a specific one). The results should be be shown in Eclipse including the path to the error if CPAchecker finds one.

  Requirements: Java, Eclipse platform

  Mentor: Thomas Lemberger

• Angular and automated tests for verification report

  CPAchecker produces as result a report about its verification work. An example can be seen here. This report is a web application based on AngularJS and D3 (description of current implementation, source). The goal of this project is to replace AngularJS with Angular and to write tests for the functionality of this report using an appropriate framework for automated tests.

  Requirements: JavaScript

  Mentor: Philipp Wendler

• Integrating SymPy into CPAchecker for Invariant Generation

  As a software verifier, many of CPAchecker's components benefit from, or even require, auxiliary information about the analyzed program, so-called invariants. Many interesting invariants, however, are difficult to derive and often require complex algebraic analysis. Fortunately, the open-source computer algebra system (CAS) SymPy already provides readily available utilities for solving algebraic problems. The goal of this project is to

  1. integrate SymPy into CPAchecker via Jython,
  2. implement a configurable program analysis (CPA) to apply SymPy to generate loop invariants for C programs, and
  3. evaluate the usefulness of these auxiliary invariants for the k‑induction verification algorithm.

  Requirements: Python, Java, Formal methods

  Mentor: Matthias Dangl

• DART-like Test-case Generation in CPAchecker

  Symbolic execution is a state-of-the-art technique for program analysis and generation of holistic test suites. It is used by many successful tools, e.g., KLEE or DART. Traditional symbolic execution suffers from exponential runtime, but DART still achieves high performance: To do so, it combines symbolic execution with concrete program execution. Our own tool CPAchecker does not use concrete execution, but abstracts unnecessary information about a program and runs symbolic execution on that abstraction. The goal of this project is to add a concrete execution component, similar to DART's, to CPAchecker's symbolic execution engine. Through this, an additional performance boost is expected, that may bring symbolic execution and test-suite generation to a new level.

  Requirements: Java, some knowledge in formal methods

  Mentor: Thomas Lemberger

• Checking Equivalence of Program Semantics Automatically

  Given two C programs, we want to know whether their semantics are the same, or different. CPAchecker supports a lot of different abstract domains for program analysis. In addition, it uses a graph-based intermediate representation for programs. This is a perfect starting point for implementing a check for semantic equivalence of two given programs! Such a check is wished for in different applications: For example regression testing, versioning systems or automatic program repair. Approaches to equivalence checking involve program inlining and symbolic analysis and building a special cross-product of the two programs for comparison. The goal of this project is to leverage the rich existing infrastructure of CPAchecker to implement an equivalence check for C programs based on these techniques.

  Requirements: Java, some knowledge in formal methods

  Mentor: Thomas Lemberger

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 SAT and SMT solvers out there that can be integrated into our library. This project aims to integrate several of them and provide bindings. We want to have an automated build process, integration tests, documentation, etc. Possible candidates are CVC4, Boolector, or Yices2.

  Requirements: Java, JNI, C/C++

  Mentor: Karlheinz Friedberger

• SMT in the Cloud

  Sometimes a local machine is too weak to solve a big SMT problem, or many SMT queries are nearly identical. The task is to implement a server-client infrastructure for solving of SMT queries with JavaSMT. To be efficient, we need normalization of formulas, caching, etc. More details can be communicated with the maintainers of JavaSMT.

  Requirements: Java, Network

  Mentor: Karlheinz Friedberger

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.

• Make use of the Intel Cache Allocation Technology

  If several benchmarking runs should be executed in parallel on the same system, the memory usage of one run can influence the performance of others (because CPU caches and the memory bandwidth is shared), even if each run gets its own reserved share of the memory. Recent Intel CPUs have a cache allocation technology, which allows to control the usage of caches and memory bandwidth and reduce the influence that parallel benchmarking runs have on each other. The goal of this project is to add support for using this technology to BenchExec (corresponding GitHub issue with more information).

  Requirements: Python, knowledge of hardware architectures, maybe C

  Mentor: Philipp Wendler

• Modern architecture and tests for HTML tables

  For the results of benchmarking runs, BenchExec produces interactive HTML tables (example) with filtering of rows, plots, etc. The JavaScript code behind these tables is old and does not have a good architecture. The goal of this project is to rewrite this code with a modern architecture and current best practices. A library such as DataTables should be used to improve the handling of large tables (with thousands of rows) and provide more features such as sorting. Furthermore, tests for the functionality of these tables should be added using an appropriate framework for automated tests. Corresponding GitHub issues for some of these tasks: #237, #130, #123, #113, #214 (full list).

  Requirements: JavaScript

  Mentor: Philipp Wendler

Instructions for Students

Students wishing to participate in Google Summer of Code must realise that this is an important professional opportunity. You will be required to produce code for an award-winning tool chain or parts of its infrastructure. Therefore, we seek students 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 in person, if needed). You should communicate with your mentor, and formally report progress and plans weekly.

Recommended steps

• Join the mailing list of a project of your choice, introduce yourself, and meet your fellow developers
• Read Google's instructions for participating and the GSoC Student Manual
• Take a look at the list of ideas
• Come up with 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

Student 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 proposal the basis of our decisions of which student to choose.

Students 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 can’t 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 Students

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.