Hendrik Tews, Tjark Weber, and Marcus Völp. In Ralf Huuck, Gerwin Klein, and Bastian Schlich, editors, Proceedings of the 3rd International Workshop on Systems Software Verification (SSV 08), Sydney, Australia, February 25-27, 2008, volume 217 of Electronic Notes in Theoretical Computer Science, pages 79-96. Elsevier, July 2008.
This paper presents our solutions to some problems we encountered in an ongoing attempt to verify the micro-hypervisor currently developed within the Robin project. The problems that we discuss are (1) efficient automatic reasoning for type-correct programs in virtual memory, and (2) modeling memory-mapped devices with alignment requirements. The discussed solutions are integrated in our verification environment for operating-system kernels in the interactive theorem prover PVS. This verification environment will ultimately be used for the verification of the Robin micro-hypervisor. As a proof of concept we include an example verification of a very simple piece of code in our environment.
@inproceedings{tews08formal,
author = {Hendrik Tews and Tjark Weber and Marcus V{\"o}lp},
title = {A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code},
editor = {Ralf Huuck and Gerwin Klein and Bastian Schlich},
booktitle = {Proceedings of the 3rd International Workshop on Systems Software Verification (SSV~2008), Sydney, Australia, February~25-27, 2008},
volume = {217},
series = {Electronic Notes in Theoretical Computer Science},
pages = {79--96},
publisher = {Elsevier},
month = jul,
year = {2008},
url = {http://dx.doi.org/10.1016/j.entcs.2008.06.043}
}
A revised version of this paper is available.