I am a second-year CSE PhD student at the University of Michigan, advised by Prof. Karem Sakallah. I received my B.S. and M.S. degree in ECE from the National Taiwan University, during which I was advised by Prof. Jie-Hong Roland Jiang.

Research Interest

My research interests are formal verification, automated reasoning, and computational logic. In particular,

Formal verification. I am generally interested in software/hardware formal verification. My current research applies automated reasoning techniques to verify safety properties of distributed protocols. In the past, I have worked on hardware model checking and our work (paper) won the first place of problem A in the 2020 CAD Contest.

Automated reasoning. I am also interested in developing automated reasoning software for applications in formal verification. I have worked on topics related to SAT/QBF solving, and I developed a certified stochastic Boolean satisfiability solving framework cert-SSAT based on a certified knowledge compilation framework CPOG.

Computational logic. Besides developing algorithms, I am also interested in proof systems and proof complexities so as to understand what makes an algorithm work well in practice despite the problem’s complexity. My master thesis focused on developing the first sound and complete proof system for a new logical formalism, dependency stochastic Boolean satisfiability (paper).

News

• Aug. 2024: I will be presenting our work Knowledge Compilation for Incremental and Checkable Stochastic Boolean Satisfiability at IJCAI 2024
• April, 2024: Our paper Knowledge Compilation for Incremental and Checkable Stochastic Boolean Satisfiability is accepted at IJCAI 2024.
• Aug., 2023: I started my Ph.D.in Computer Science and Engineering at University of Michigan, Ann Arbor.
• July, 2023: I successfully defended my master’s thesis (slides) and received M.S. in ECE from National Taiwan University.
• Jan., 2023: I was admitted to the Ph.D. program in Computer Science and Engineering at University of Michigan, Ann Arbor.
• May, 2023: Our paper A Resolution Proof System for Dependency Stochastic Boolean Satisfiability is accepted at Journal of Automated Reasoning.
• July, 2021: Our paper Compatible Equivalence Checking of X-Valued Circuits is accepted at ICCAD 2021.
• June, 2021: I received my B.S. in ECE from National Taiwan University.

For more info

Welcome to take a look at my publication list for more information about my research. To me, the most wonderful apsect of research is building solutions to real-world challenges upon fundamental basis and understanding them. I would also be very happy to meet friends with common research interests.