Yun-Rong Lauren Luo
yunrong AT umich DOT edu

I am a first-year CSE PhD student at the University of Michigan, advised by Prof. Karem Sakallah. I have a general interest in formal verification, automated reasoning, and computational logic.

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.

Google Scholar  /  Twitter  /  Github

profile photo
Research

My past research is related to theory, practice, and application of satisfiability (SAT) solving. My recent work Resolution for DSSAT presents the first sound and complete resolution proof system for Dependency Stochastic Boolean Satisfiability (DSSAT). My previous work X-Value Equivalence Checking presents our compatible equivalence checking algorithm for circuits with X-value, which won the first place in Problem A of 2020 ICCAD CAD Contest.

A Resolution Proof System for Dependency Stochastic Boolean Satisfiability
Yun-Rong Luo, Che Cheng, Jie-Hong Roland Jiang
Journal of Automated Reasoning, 2023
Paper

Dependency stochastic Boolean satisfiability (DSSAT) is a logical formalism that allows compact encoding of NEXPTIME decision problems under uncertainty. We present the first sound and complete resolution calculus for DSSAT which may pave a theoretical foundation for further development and certification of DSSAT solvers.

Compatible Equivalence Checking of X-Valued Circuits
Yu-Neng Wang, Yun-Rong Luo, Po-Chun Chien, Ping-Lun Wang, Hao-Ren Wang, Wan-Hsuan Lin, Jie-Hong Roland Jiang, Chung-Yang Ric Huang
ICCAD, 2021
Paper

The challenge of equivalence checking for X-valued circuits (compatible equivalence checking), is posed in the 2020 ICCAD CAD Contest. We present our winning method based on X-value preserving dual-rail encoding.

This website uses the html template by Jon Barron.