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 001; Hsiang-Shang Ko; Yu-Fang Chen 001 (OSDI, 2020)

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)

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)