Software and Computational Systems Lab at LMU Munich

Mentors: Student: Wenyi Shi

CPA-Daemon is a microservice (currently gRPC service) for continuous verification of C programs with CPAchecker. Clients could craft gRPC requests (with details for instructing a CPAchecker program run) sending to CPA-Daemon and receive the program-verification response. Current CPA-Daemon integration tests require large inputs that are difficult to read within code: c input programs, CPAchecker specifications, CPAchecker configurations[3]. So our goal in this project is "A running integration-test suite for CPA-Daemon based on Cucumber". With Cucumber clear "Given / When / Then" semantics in writing test, we aim to reach the same or more branch coverage than the existing integration tests. Adopt Cucumber should help us easily add more test in the future.

Mentors: Student: Patrik Felbinger

This project developed a machine-learning framework to predict the most effective software verifier for a given C program – trained on the Software Verification Competion (SV-COMP) 2025. The system comprises Verifier-Moira, a modular library for selecting verifiers using program embeddings (e.g., GraphCodeBERT) and predictors (e.g., LightGBM, XGBoost, neural classifier), and Verifier-Moira-Data, a repository for training and publishing predictors. Evaluations show that predictors consistently outperform the best verifier-per-property baseline. Together, the two repositories offer a unique, fully integrated solution: one for training predictors, the other for applying them efficiently to real programs.

Mentors: Student: Ahmed Tarek

PJBDD is a Java-based, multi-threaded Binary Decision Diagram (BDD) library that facilitates concurrent computation and parallel operations. It is specifically designed to enable efficient manipulation of Boolean formulas. This project aims to introduce a new type of decision diagram that is expected to improve performance by incorporating more reduction rules than existing ones called CESRBDD( binary decision diagrams with complemented edges and edge-specified reductions).

Mentors: Student: Zhengyang Lu

We developed the first algorithm selector, Btor2-Select, for the word-level hardware model-checking problem described in the Btor2 language. Given a Btor2 instance, Btor2-Select selects and applies the expected best verifier(s) from a pool of hardware and software tools. These decisions are based on various machine learning (ML) models, trained upon historical performance data, mapping from instance features to algorithm selections. We proposed two embeddings for Btor2 instances: bag of keywords and bit-width aggregation. Two traditional algorithm-selection ML models, i.e., empirical hardness model and pairwise classifiers, were implemented in Btor2-Select. More importantly, we developed a novel algorithm selection and scheduling framework based on deep reinforcement learning (RL). This RL framework allows for adaptive algorithm selection throughout the solving process, leveraging dynamic information such as previous attempts and elapsed time. Upon evaluation, the adaptive algorithm selector outperformed the best non-portfolio solver (SBS) by 24.4%. Moreover, it closed 6.69% more SBS-VBS gaps than the best non-adaptive algorithm-selection method, a common performance indicator for algorithm selectors. All the codes, experiments, and data can be found at: https://gitlab.com/sosy-lab/software/btor2-select.

Mentors: Student: Haoran Yang

For benchmarking purposes, BenchExec typically creates a container with a file-system overlay atop the system's file system. However, due to a kernel change, this process is no longer viable for the root file system. Implementing fuse-overlayfs as an alternative overlay mechanism might resolve this issue. This entails developing a fallback mechanism for BenchExec's file-system overlay strategy: initially attempting to utilize the kernel overlayfs, and if unsuccessful, resorting to fuse-overlayfs. This approach ensures BenchExec's functionality remains intact.