Hendrik Tews, Marcus Völp, and Tjark Weber. Journal of Automated Reasoning: Special Issue on Operating Systems Verification, 42(2-4):189-227, April 2009.
This article contributes to the field of operating-systems verification. It presents a formalization of virtual memory that extends to memory-mapped devices. Our formalization consists of a stack of three detailed formal memory models: physical memory (i.e., RAM), physically-addressable memory-mapped devices (including their respective side effects, access and alignment requirements), and page-table based virtual memory. Each model is formally shown to satisfy the plain-memory specification, a memory abstraction that enables efficient reasoning for type-correct programs.
This stack of memory models was developed in an attempt to verify Nova, the Robin micro-hypervisor. It is a key component of our verification environment for operating-system kernels based on the interactive theorem prover PVS.
@article{tews09formal,
author = {Hendrik Tews and Marcus V{\"o}lp and Tjark Weber},
title = {Formal Memory Models for the Verification of Low-Level Operating-System Code},
journal = {Journal of Automated Reasoning: Special Issue on Operating Systems Verification},
volume = {42},
number = {2--4},
pages = {189--227},
month = apr,
year = {2009},
url = {http://dx.doi.org/10.1007/s10817-009-9122-0}
}