We are hiring new doctoral researchers, student research assistants, and tutors. Apply now!
Distinguished Paper Award and Best Artifact Award at FSE 2024!

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)

Room
F 005
Office Hours
by appointment, please send me an e-mail in advance
Email
firstname.lastname@sosy.ifi.lmu.de
(please write me in English)
ORCID
0000-0001-5139-5178
Personal Homepage
CV
DBLP
Google Scholar
GitLab
GitHub

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
Btor2 Frontend for CPAchecker

Background: Btor2 [1] is a bit-precise language that models word-level sequential circuits, and has been adopted by the Hardware Model Checking Competition. Btor2C [2] 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, e.g. CPAchecker. A Btor2 bit-vector can have an arbitrary width, and Btor2C encodes it with the shortest possible C integer. Thus, the C-integer variable might have some redundant bits, which complicates the analysis and harms the performance of software verifiers.

Goal: In this project, we want to implement a new frontend in CPAchecker to parse a Btor2 verification problem and represent it as a control-flow automaton. With this new frontend, CPAchecker could analyze a Btor2 circuit directly and (hopefully) more efficiently.

Requirements: (general information)

  • Ability to program in Java
  • Basic knowledge of Kripke structure and SAT/SMT solving

Validation-via-Verification for Hardware Btor2 Circuits

Background: Btor2 [1] is a bit-precise language that models word-level sequential circuits, and has been adopted by the Hardware Model Checking Competition. Btor2C [2] 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. If a software verifier finds an error in the program, it generates a violation witness, which records the execution path leading to that error. On the other hand, if a software verifier proves a program correct, it generates a correctness witness [3] containing some program invariants that could reconstruct a correctness proof.

Goal: The goal of this project to certify the correctness witnesses (in GraphML format) produced by software verifiers by following the validation-via-verification approach [4]. The original Btor2 circuit is instrumented with the invariants from a correctness witness, and can then be independently solved by hardware verifiers.

Requirements: (general information)

  • Ability to program in Python (, Java, and/or C)
  • Basic knowledge of Kripke structure and SAT/SMT solving

Violation Witness Translation from C to Btor2

Background: Btor2 [1] is a bit-precise language that models word-level sequential circuits, and has been adopted by the Hardware Model Checking Competition. Btor2C [2] 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. If a software verifier finds an error in the program, it generates a violation witness [3], which records the execution path leading to that error. On the other hand, if a software verifier proves a program correct, it generates a correctness witness containing some program invariants that could reconstruct a correctness proof.

Goal: The goal of this project to translate the violation witnesses in GraphML format produced by software verifiers to Btor2 format, such that one could use hardware simulators to validate them.

Requirements: (general information)

  • Ability to program in Python (, Java, and/or C)
  • Basic knowledge of Kripke structure and SAT/SMT solving

Support Bit-Precise Integer Representation in CPAchecker for Btor2 Verification Tasks

Background: Btor2 [1] is a bit-precise language that models word-level sequential circuits, and has been adopted by the Hardware Model Checking Competition. Btor2C [2] 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, e.g. CPAchecker. A Btor2 bit-vector can have an arbitrary width, and Btor2C encodes it with the shortest possible C integer. Thus, the C-integer variable might have some redundant bits, which complicates the analysis and harms the performance of software verifiers.

Goal: The goal of this project is to support bit-precise integer representation in CPAchecker specifically for these hardware-verification tasks. One possible way to achieve this is by defining a customized C annotation such that CPAchecker can infer the precise bit-width.

Requirements: (general information)

  • Ability to program in Java and C
  • Basic knowledge of Kripke structure and SAT/SMT solving

Currently assigned topics
Algorithm Selection for Btor2 Verification Tasks using Circuit Structure Information

Background: Btor2 [1] is a bit-precise language that models word-level sequential circuits, and has been adopted by the Hardware Model Checking Competition. Btor2C [2] 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.

Goal: Now that a large collection of tools from both hardware and software verification communities are at our disposal, we want to combine forces of them via machine learning (ML). The objective is to construct a selector using information of the Btor2 circuit structure [3], and train it on a large Btor2 dataset. Given a Btor2 task, the ML-based selector can then predict the best-suited tool/algorithm(s) for solving it.

Requirements: (general information)

  • Ability to program in Python
  • Basic knowledge of graph kernel, Kripke structure, and SAT/SMT solving
  • Practical knowledge of support vector machine, decision/boosting tree, and random forest

Finished topics
Reverse Program Synthesis for Backward Reachability Analysis

Description: 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.

Requirements: (general information)

  • Ability to program in Java and understand C code
  • Basic knowledge of control-flow automata

Improving the Encoding of Arrays in Btor2-to-C Translation

Background: Btor2 [1] is a bit-precise language that models word-level sequential circuits, and has been adopted by the Hardware Model Checking Competition. Btor2C [2] 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 analyzers. Currently, on every write of an array, Btor2C creates a copy of it, even when unnecessary (see this issue). This might put burdens on software analyzers and hinders their performance.

Goal: The goal of this project is to alleviate such situation and allocate a new array only when necessary. Additionally, we also want to implement a translator that converts Btor2 array tasks to pure bit-vector tasks by blasting the array operations (read and write) into a chain of ite operations.

Requirements: (general information)

  • Ability to program in C (and/or Python)
  • Basic knowledge of Kripke structure and SAT/SMT solving

Awards

Publications

Projects

Teaching