Welcome to my personal website!

News

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

Short Biography

I am on the academic job market! Here are my

• CV
• Publication list
• 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.

I enjoy doing research and collaborating with people from different countries. During my doctoral study, I was

• a visiting student on DAAD scholarship at LMU Munich, Germany (September 2019 - August 2020),
• an internship student at National Institute of Informatics, Tokyo, Japan (September 2018 - February 2019), and
• a research intern at IBM T. J. Watson Research Center, New York, U.S.A. (July - October 2016).

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