Toward the Verification of a Simple Hypervisor - Mike Dahlin; Ryan Johnson 003; Robert Bellarmine Krug; Michael McCoyd; William D. Young (ACL2, 2011)