Po-Chun Chien / 錢柏均
Software and Computational Systems Lab
Department of Computer Science
Ludwig-Maximilians-Universität München (LMU Munich)
80538 Munich (Germany)
- Room F 005, Oettingenstr. 67
- Office hours
- by appointment, please send me an e-mail in advance
- Personal Homepage
Please send me encrypted mails!
My GPG key: 0xBF5174377577E298
Fingerprint: E9A3 CF7F C45B BDE1 17A9 BFE5 BF51 7437 7577 E298
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.
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. One could then apply existing analysis to verify the reverse CFA.
Background: Btor2 is a bit-precise language that models word-level sequential circuits, and has been adopted by the Hardware Model Checking Competition. Btor2C is a hardware-to-software translator that converts circuits in Btor2 format to C programs. With Btor2C, one could analyze hardware designs with off-the-shelf software verifiers or testers. Goal: The goal of the project is to compare the performance between software and hardware analyzers and try to improve Btor2C based on the findings. A few possible directions are
- Analyze the performance difference between software and hardware verifiers
- Define a customized C annotation for bit-precise integer/bit-vector encoding, and have it implemented in Btor2C and CPAchecker
- Improve Btor2C array encoding (see https://gitlab.com/sosy-lab/software/btor2c/-/issues/17)
- Support witness format conversion in Btor2C
Implement Backward symbolic execution in CPAchecker 
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.
Implement single-loop transformation in CPAchecker 
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.
Evaluate the robustness of SV-COMP benchmark set and participating tools
The idea is to mutate (e.g. by negating the assertions) the tasks in SV-COMP benchmark set, and see if the verifiers still deliver the expected results on the mutated tasks. If not, it indicates that the tool might be unsound, or the verdicts might be incorrect. In either case, we could improve the robustness of SV-COMP.
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.
- CPAchecker: The Configurable Software-Verification Platform
- Btor2C: A converter from word-level verification tasks in the Btor2 format to C programs
- WS 2022/23: Bachelorseminar: "Software Verification: Tools and Techniques"
- SS 2022: Praktikum Software Engineering für Fortgeschrittene
- WS 2021/22: Software Verification
- WS 2021/22: Planmäßige Entwicklung eines größeren Softwaresystems