Sciweavers

ENTCS
2008

A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code

13 years 3 months ago
A Formal Model of Memory Peculiarities for the Verification of Low-Level Operating-System Code
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.
Hendrik Tews, Tjark Weber, Marcus Völp
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where ENTCS
Authors Hendrik Tews, Tjark Weber, Marcus Völp
Comments (0)