Software and Computational Systems Lab at LMU Munich

The Software and Computational Systems Lab is a research group at LMU Munich, one of the leading universities in Germany. We focus on the development of new models and algorithms to efficiently analyze software systems and emphasize on tool implementations of the theoretical concepts. For GSoC 2024, we propose ideas involving several aspects of software analysis, from implementing and benchmarking verification algorithms to incorporating backend logic solvers.

Here is a selection of the open-source projects developed by our group:

• CPAchecker is an

award-winning framework for formal verification of C programs. It is written in Java and based on a highly modular architecture that allows one to develop and combine a wide range of different analyses. CPAchecker has helped to find hundreds of bugs in the Linux kernel. •

• CPA-Daemon is a gRPC-based microservice that enables users to run CPAchecker in a cloud setup, with a focus on ease of use and continuous verification.

• JavaSMT is a common API layer for accessing various SMT solvers

from Java programs without having to use solver-specific APIs and care about subtle details. It supports the majority of common SMT solvers and is used by a wide range of projects.

• PJBDD is a multi-threaded

Binary Decision Diagram (BDD) library written in Java. It supports concurrent computation, parallel operations, and automated resource management.

• BenchExec is a benchmarking framework (written in Python)

that uses modern Linux features such as cgroups and namespaces to create benchmarking containers and measure their resource usage.

For a more detailed description and some prospective GSoC topics, please visit our webpage. You are also welcome to suggest your own ideas!