| permalink | title | excerpt | author_profile | redirect_from | ||
|---|---|---|---|---|---|---|
/ |
Welcome to my personal website! |
About me |
true |
|
I will join the EE department of National Taiwan University as Assistant Professor from February 2025!
- Information for prospective students: slides
I am looking for prospective Ph.D. students to work on the verification of hardware and software systems. The project is funded by the German Research Foundation (DFG). Please refer to the slides for more information.
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.
Here are my:
- 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.
- 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.
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 CBtor2-Cert: a certifying hardware verifier using software analyzersCPV: a circuit-based program verifierMoXIchecker: the first direct model checker for the modeling language MoXIreSSAT,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
My email address: [email protected]
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