Welcome to my personal website!
News
- 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
- 2022-12-23: Our paper Bridging hardware and software analysis with Btor2C: A word-level-circuit-to-C translator is accepted at TACAS 2023
Short Biography
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).
To know more about me, please take a look at my CV.
Recent Publications
The following are some of my recent publications. Please refer to my publication list or click the Publications button on the top menu for the complete list.
2023
- Bridging hardware and software analysis with Btor2C: A word-level-circuit-to-C translator (TACAS)
- Translating word-level Btor2 circuits to C programs and applying software analysis
- A supplementary webpage for an author copy of the paper and for browsing the experimental results
- A reproduction package for the conducted experiments
2022
- Interpolation and SAT-based model checking revisited: Adoption to software verification
- Adoption of McMillan’s 2003 algorithm for interpolation-based model checking to software verification
- A supplementary webpage for browsing the experimental results
- A reproduction package for the conducted experiments
2021
- Stochastic Boolean satisfiability: Decision procedures, generalization, and applications (Doctoral dissertation)
- An author copy of the dissertation
- A supplementary reproduction package for the evaluation
- Dependency stochastic Boolean satisfiability: A logical formalism for NEXPTIME decision problems with uncertainty (AAAI)
2020
- Constraint solving for synthesis and verification of threshold logic circuits (IEEE Trans. CAD)
- Engineering change order for combinational and sequential design rectification (DATE)
- Collaboration with Dr. Victor N. Kravets from IBM Research
2019
- Stability analysis for safety of automotive multi-product lines: A search-based approach (GECCO)
- Collaboration with Dr. Paolo Arcaini and Prof. Fuyuki Ishikawa from NII, and Dr. Shaukat Ali from Simula Research Laboratory
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 CreSSAT,erSSAT: solvers for the random-exist and exist-random quantified fragments of stochastic Boolean satisfiabilityssat-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 toolABC
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
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