Welcome to my personal website!

I am looking for Ph.D., Master’s, and Bachelor’s students to work on formal methods!

• Information for prospective students: slides
• Ph.D. students may be enrolled at LMU Munich (project funded by DFG).

Short Biography

I am an Assistant Professor at the Department of Electrical Engineering of National Taiwan University, Taiwan, and a “Gastprofessor” (Guest Professor) affiliated with Software and Computational Systems Lab at LMU Munich, Germany. I obtained a Ph.D. degree in Electronics Engineering from National Taiwan University in 2021. My research directions are the analysis and optimization of computing systems, with a focus on formal methods.

Here are my:

• CV
• Publication list
• Research statement
• Teaching experience

News

• 2025-02-01: I joined National Taiwan University as an Assistant Professor.
• 2025-01-23: I was appointed as a “Gastprofessor” (Guest Professor) at LMU Munich, Germany.
• 2024-07-15: Our FSE 2024 paper A transferability study of interpolation-based hardware model checking for software verification and its reproduction package won the ACM SIGSOFT Distinguished Paper Award and Best Artifact Award.
• 2024-04-11: Our TACAS 2024 paper Btor2-Cert: A certifying hardware-verification framework using software analyzers won the Distinguish Artifact Award (cf. reproduction package).
• 2024-04-10: Our SPIN 2024 paper Augmenting interpolation-based model checking with auxiliary invariants won the Best Paper Award.
• 2024-03-28: Our grant proposal Bridging Hardware and Software Analysis was approved by the German Research Foundation (DFG)! See the slides of my talk at COOP 2024 for more details.

Software Projects

I am the primary designer and maintainer of the following projects:

• Btor2C: a translator from the word-level modeling language Btor2 to the programming language C
• Btor2-Cert: a certifying hardware verifier using software analyzers
• CPV: a circuit-based program verifier
• MoXIchecker: the first direct model checker for the modeling language MoXI
• reSSAT, erSSAT: solvers for the random-exist and exist-random quantified fragments of stochastic Boolean satisfiability
• ssat-benchmarks: a collection of stochastic Boolean satisfiability formulas for benchmarking (Contributions Welcome!)
• TLCollapseVerify: collapse operation and efficient verification of threshold logic in a synthesis/verification tool ABC

I participate in the following projects:

• CPAchecker: a configurable software-verification platform
  • Design and implementation of McMillan’s interpolation-based model-checking algorithm
• BenchExec: a reliable and precise benchmarking framework
  • Incorporation SAT solver Kissat and ABC

Contact

My email address: nian-ze.lee@sosy.ifi.lmu.de

Please send me encrypted emails!

My GPG key can be downloaded from the Keys OpenPGP server. Fingerprint: 6211 DD38 D7BD 0167 253B B4F8 EBA3 A3F7 F4F9 BBEC