Yao Hsiao

Yao Hsiao

Electrical Engineering Ph.D. Student

Stanford University


I am an Electrical Engineering Ph.D. Student at Stanford University advised by Professor Caroline Trippel. I am currently working on the intersection of microarchitecture and formal methods.

My recent project is in automatically synthesizing formal models of hardware from RTL for efficient hardware Memory Consistency Model (MCM) verification. A growing body of work has proposed the use of abstract formal models in verification of correctness and security properties of hardware. The work bridges the gap between these proposed abstraction and the actual hardware implementation written in RTL, and thus allows prior work deployable on actual hardware.

Prior to graduate school, I received BS degree in Electrical Engineergin from National Tsing Hua University.

  • Computer Architecture
  • Formal Verification
  • PhD in Electrical Engineering, 2026

    Stanford University

  • BSc in Electrical Engineering, 2020

    National Tsing Hua University


(2021). Synthesizing Formal Models of Hardware from RTL for Efficient Verification of Memory Model Implementations. MICRO'21.

PDF Cite Code Video DOI

(2020). Determinizing Crash Behavior with a Verified Snapshot-Consistent Flash Translation Layer. OSDI'20.

PDF Cite Code