Software and Computational Systems Lab
Department of Computer Science
Ludwig-Maximilians-Universität München (LMU Munich)
80538 Munich (Germany)
- Room F 009, Oettingenstr. 67
- Office Hours
- By appointment
Please send me encrypted mails!
My GPG key: 0x0C6A6D6A013FD4CF
Fingerprint: DAF8 96DE 3569 D688 C46D BC0E 0C6A 6D6A 013F D4CF
Tubes: Identifying Abstract Error Traces
There might be several reasons for reaching a specific error location in a program. We want to identify all classes of inputs that trigger the same bug. They should be as abstract as possible but as precise as necessary. For a given program we want to find out, which restrictions to nondeterministic variables are necessary to reach an error location. For example, we might reach error location E1, if the nondeterministic variable x equals 1 and the nondeterministic variable y is less than 1024. Error location E2 might be reachable for x > 100 and y < 100. Otherwise the program does not show faulty behavior. In our approach we are interested in the most abstract restrictions for all inputs for reaching error locations instead of a single testvector like x = 1 & y = 1023 for E1 and/or x = 101 & y = 99 for E2.
Correctness Witnesses are an artifact produced by a verifier which allows a validator to replay the verification process. The task would be to analyze correctness witnesses and find semantically equivalent witnesses from the perspective of a validator.
Modular Distributed Summary Synthesis
Due to the rising availability of distributed computational power distributing a verifier is of great interest. While distributing a single verifier is important, we consider how to use verifiers as building blocks in order to achieve distributed verification. Your goal would be to create a framework to make this possible, based upon some existing theory.
Currently assigned topics
Scaling Formal Verification: Parallel Analysis of Functions in CPAchecker 
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 in multiple smaller tasks that are then verified in parallel. As soon as one of the analyses reports a violation, we abort all other analyses and report the violation. This will lead to many false alarms since we do not know with which input parameters functions will be called. Return values of functions will be ignored and interpreted as unknown value in a first step. From there we can continue in two directions:
- 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])
- We identify each function call automatically and try to infer all parameters.
- The verification verdict should be available faster (in terms of passed walltime).
- Wrong proofs should be non-existing. In case a program is safe, the decomposition should be a sound over-approximation.
CPAchecker is a framework for automatic software verification developed at our chair. As such it has a broad technology stack that should provides everything that is needed for verifying C programs. CPAchecker is able to distribute the analysis of a single task to different workers by decomposing the input program into blocks. Each worker analyzes one block and communicates the results to all other workers over messages to establish the correct verification result. In case we find a violation, fault localization can help to explain the root cause of the error. There already exist several techniques of fault localization in CPAchecker. Unfortunately, some of them may take long since they have to check 2^n possibilities in the worst-case scenario. By distributing fault localization to the relevant workers, 'n' shrinks since they work on smaller blocks. We expect a performance boost for fault localization after distributing it.
Reconstruction of Violation and Correctness Witnesses for Distributed Block Summaries 
CPAchecker is a framework for automatic software verification developed at our chair. As such it has a broad technology stack that should provides everything that is needed for verifying C programs. CPAchecker is able to distribute the analysis of a single task to different workers by decomposing the input program into blocks. Each worker analyzes one block and communicates the results to all other workers over messages to establish the correct verification result. In case we find a violation, we want to provide the user with a counterexample that proves the reachability of a violation. Currently, neither the counterexample nor invariants can be synthesized from the messages. However, witnesses are important for improving the trust in the verfication results.
The SV-COMP benchmarks set is one of the largest benchmarks sets of C programs for software verification. For all programs in the set we know whether the program fulfills certain properties, e.g., the function 'reach_error' is never called. The benchmarks help to evaluate state-of-the-art verification tools and their effectiveness. For fault localization techniques there is no large benchmark set that provides sufficient metadata for each task to perform a large-scale evaluation. The idea is to create such tasks by manually crafting them, injecting faults in safe tasks, or identifiying fixes for unsafe tasks.
If you're a student interested in writing your thesis at our chair, you should also have a look at our full list of currently available theses.
- WS'24: Bachelorseminar: "Validation of Verification Results"
- SS'23: Praktikum Software Engineering für Fortgeschrittene
- SS'23: Bachelorseminar: "Machine Learning in Software Engineering"
- WS'22: Semantik von Programmiersprachen
- WS'22: Bachelorseminar: "Software Verification: Tools and Techniques"
- SS'22: Praktikum Software Engineering für Fortgeschrittene