yaohsiao@stanford.edu
I am an Electrical Engineering Ph.D. Student at Stanford University advised by Prof. Caroline Trippel. My research interests are in computer architecture (microarchitecture, memory system, concurrency, and security) and formal methods.
One project is in automatically synthesizing formal models of hardware from RTL for efficient hardware Memory Consistency Model (MCM) verification. Another project proposed the first automated approach and tool for characterizing side channels on hardware. Recent on-going projects include verification on cache hierarchy and design for verification.
Prior to graduate school, I received B.S. degree in Electrical Engineergin from National Tsing Hua University. During my undergraduate studies, I had worked with Dr. Yu-Fang Chen at Academia Sinica, Prof. Jing-Jia Liou, and Prof. Ren-Shuo Liu.
RTL2MμPATH: Multi-μPATH Synthesis with Applications to
Hardware Security Verification.
Yao Hsiao, Nikos Nikoleris, Artem Khyzha, Dominic P.
Mulligan, Gustavo Petri, Christopher W. Fletcher, Caroline
Trippel.
MICRO 2024
paper / cite
/ code
Synthesizing Formal Models of Hardware from RTL for
Efficient Verification of Memory Model Implementations.
Yao Hsiao, Dominic P. Mulligan, Nikos Nikoleris,
Gustavo Petri, Caroline Trippel.
MICRO 2021
paper / cite
/ code / vidoe
/ doi
Determinizing crash behavior with a verified
snapshot-consistent flash translation layer.
Yun-Sheng Chang, Yao Hsiao, Tzu-Chi Lin, Che-Wei Tsao,
Chun-Feng Wu, Yuan-Hao Chang, Hsiang-Shang Ko, and Yu-Fang Chen.
OSDI 2020
paper / cite
/ code +
proof