Welcome to my personal website!

I am looking for prospective Ph.D. students to work on the verification of hardware and software systems, funded by the German Research Foundation (DFG). Please refer to the slides for more information.

Short Biography

I am on the academic job market! Here are my

• CV
• Publication list
• Research statement
• Teaching experience

I am a postdoctoral researcher 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.

News

• 2024-06-22: Our paper A transferability study of interpolation-based hardware model checking to software verification and its reproduction package win the ACM SIGSOFT Distinguished Paper Award and Distinguished Artifact Award at FSE 2024.
• 2024-04-15: Our paper A transferability study of interpolation-based hardware model checking to software verification is accepted at FSE 2024.
• 2024-03-28: Our grant proposal is approved by the German Research Foundation (DFG)! We are hiring a Ph.D. student to work on bridging hardware and software formal verification.
• 2024-02-27: Our paper Augmenting interpolation-based model checking with auxiliary invariants is accepted at SPIN 2024 and receives the Best Paper Award (2024-04-10).
• 2023-12-22: Our paper Btor2-Cert: A certifying hardware-verification framework using software analyzers is accepted at TACAS 2024; its reproduction package is awarded the Distinguish Artifact Award (2024-04-11).
• 2023-12-05: Our verifier CPV ranks 6th (out of 26 tools) as a first-time participant in the category ReachSafety at SV-COMP 2024.
• 2023-09-11: I organized the 8th International Workshop on CPAchecker.
• 2023-09-04: I mentored a project in the Google Summer of Code 2023.
• 2023-07-06: Our paper Interpolation and SAT-based model checking revisited: Adoption to software verification is accepted by Journal of Automated Reasoning.
• 2023-07-06: Our paper CPA-DF: A tool for configurable interval analysis to boost program verification is accepted at ASE 2023.

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
• 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