In the paper we examine one of the issues in designing, specifying, implementing and formally verifying a small operating system kernel -- how to provide a productive and iterative development methodology for both operating system developers and formal methods practitioners.
We espouse the use of functional programming languages as a medium for prototyping that is readily amenable to formalisation with a low barrier to entry for kernel developers, and report early experience in the process of designing and building \sel4: a new, practical, and formally verified microkernel.
@InProceedings{Elphinstone_KDRH_07,
author = {Kevin Elphinstone and Gerwin Klein and Philip Derrin
and Timothy Roscoe and Gernot Heiser},
title = {Towards a Practical, Verified Kernel},
booktitle = {Proc.\ 11th Workshop on Hot Topics in Operating Systems},
year = 2007,
pages = 6,
address = {San Diego, CA, USA},
month = may,
note = {Online proceedings at \url{http://www.usenix.org/events/hotos07/tech/}
}