Verifying shadow page table algorithms. - Eyad Alkassar; Ernie Cohen; Mark A. Hillebrand; Mikhail Kovalev; Wolfgang J. Paul (FMCAD, 2010)

Verification of TLB Virtualization Implemented in C. - Eyad Alkassar; Ernie Cohen; Mikhail Kovalev; Wolfgang J. Paul (VSTTE, 2012)

TLB virtualization in the context of hypervisor verification. - Mikhail Kovalev (2013)

Store Buffer Reduction with MMUs. - Geng Chen; Ernie Cohen; Mikhail Kovalev (VSTTE, 2014)

A Pipelined Multi-core MIPS Machine - Hardware Implementation and Correctness Proof. - Mikhail Kovalev; Silvia M. Müller; Wolfgang J. Paul (Springer, 2014)