I am pleased to announce that the paper “Synthesizing formal models of hardware from RTL for efficient verification of memory model implementations” has been accepted for publication at the IEEE/ACM International Symposium on Microarchitecture (MICRO) 2021. This is a paper co-written with Yao Hsiao (Stanford), Gustavo Petri (Arm Research), Nikos Nikoleris (Arm Research), and Caroline Trippel (Stanford).