Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution. - Karl Palmskog; Xiaomo Yao; Ning Dong; Roberto Guanciale; Mads Dam (FMCAD, 2022)