We are hiring new student research assistants and tutors. Apply now!
Paper accepted at ICSE 2023: "CoVeriTeam Service: Verification as a Service"

Po-Chun Chien / 錢柏均

Picture of Po-Chun Chien / 錢柏均

Software and Computational Systems Lab
Department of Computer Science
Ludwig-Maximilians-Universität München (LMU Munich)
Oettingenstraße 67
80538 Munich (Germany)

Office
Room F 005, Oettingenstr. 67
Office hours
by appointment, please send me an e-mail in advance
E-Mail
firstname.lastname@sosy.ifi.lmu.de
Personal Homepage
po-chun-chien.github.io
ORCID
0000-0001-5139-5178

GPG-Key

Please send me encrypted mails!
My GPG key: 0xBF5174377577E298
Fingerprint: E9A3 CF7F C45B BDE1 17A9 BFE5 BF51 7437 7577 E298

Thesis Mentoring

Available topics
Implement Dual Approximated Reachability algorithm in CPAchecker [1, 2]

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 [1]

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.

Performance comparison of hardware and software analyzers [1, 2]

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 [1]

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 [1]

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.

Publications

Projects

Teaching