A Secure and Formally Verified Linux KVM Hypervisor. - Shih-Wei Li; Xupeng Li; Ronghui Gu; Jason Nieh; John Zhuang Hui (SP, 2021)

Formally Verified Memory Protection for a Commodity Multiprocessor Hypervisor. - Shih-Wei Li; Xupeng Li; Ronghui Gu; Jason Nieh; John Zhuang Hui (USENIX Security Symposium, 2021)