| Synthesizing formal models of hardware from RTL for efficient verification of memory model implementations Y Hsiao, DP Mulligan, N Nikoleris, G Petri, C Trippel MICRO-54: 54th annual IEEE/ACM international symposium on microarchitecture …, 2021 | 22 | 2021 |
| Determinizing Crash Behavior with a Verified {Snapshot-Consistent} Flash Translation Layer YS Chang, Y Hsiao, TC Lin, CW Tsao, CF Wu, YH Chang, HS Ko, ... 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI …, 2020 | 5 | 2020 |
| Scalable assurance via verifiable hardware-software contracts Y Hsiao, DP Mulligan, N Nikoleris, G Petri, C Trippel First Workshop on Open-Source Computer Architecture Research (OSCAR), 2022 | 3 | 2022 |
| RTL2MμPATH: Multi-μPATH Synthesis with Applications to Hardware Security Verification Y Hsiao, N Nikoleris, A Khyzha, DP Mulligan, G Petri, CW Fletcher, ... 2024 57th IEEE/ACM International Symposium on Microarchitecture (MICRO), 507-524, 2024 | 1 | 2024 |
| Synthesizing Formal Speculation Contracts XK Li, Y Hsiao, C Trippel | | |