Hendrik Tews, Tjark Weber, Marcus Völp, Erik Poll, Marko van Eekelen, and Peter van Rossum. Technical Report ICIS-R08012, Radboud University Nijmegen, May 2008.
In this document we describe the work performed in the Robin project towards verifying the Nova micro-hypervisor operating-system kernel. In particular, we describe in detail the Robin verification environment and the results obtained with it. The Robin verification environment consists of the interactive theorem prover PVS, an IA32 (x86) hardware model in PVS, a semantics of (a rich subset of) C++, and a semantics compiler translating C++ sources into their semantics in PVS.
@techreport{tews08verification,
author = {Tews, Hendrik and Weber, Tjark and V{\"o}lp, Marcus and Poll, Erik and Eekelen, Marko van and Rossum, Peter van},
title = {{Nova} Micro--Hypervisor Verification},
number = {ICIS--R08012},
institution = {Radboud University Nijmegen},
month = may,
year = {2008}
}