We are hiring new student research assistants and tutors. Apply now!
4 papers accepted at SPIN 2024!

Nian-Ze Lee

Ph.D. / National Taiwan University

Picture of Nian-Ze Lee

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
E-Mail
firstname.lastname@sosy.ifi.lmu.de
Office Hours
By appointment
Personal Homepage
https://nianzelee.github.io/
ORCID
0000-0002-8096-5595

GPG-Key

Please send me encrypted mails!
My GPG key: 0xEBA3A3F7F4F9BBEC (from key server)
Fingerprint: 6211 DD38 D7BD 0167 253B B4F8 EBA3 A3F7 F4F9 BBEC

Thesis Mentoring

Available topics
Algorithm Selection for Btor2 Verification Tasks using Circuit Structure Information [1, 2, 3]

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

Algorithm Selection for Btor2 Verification Tasks using Syntactic Features [1, 2]

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 syntactic features of a Btor2 circuit, e.g. the numbers of certain operations, 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 Kripke structure and SAT/SMT solving
  • Practical knowledge of support vector machine, decision/boosting tree, and random forest

Btor2 Frontend for CPAchecker [1, 2]

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

Support Bit-Precise Integer Representation in CPAchecker for Btor2 Verification Tasks [1, 2]

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

Finished topics
Improving the Encoding of Arrays in Btor2-to-C Translation [1, 2]

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

Validation-via-Verification for Hardware Btor2 Circuits [1, 2, 3, 4]

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 [1, 2, 3]

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

Implement Backward Bounded Model Checking in CPAchecker [1]

Description: Bounded model checking (BMC) 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 BMC, 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.

Requirements: (general information)

  • Ability to program in Java and understand C code
  • Basic knowledge of SAT/SMT solving and weakest precondition

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, Theses, and Projects