Towards a Practical, Verified Kernel

Select |




Print


Elphinstone, Kevin; Klein, Gerwin; Derrin, Philip; Roscoe, Timothy; Heiser, Gernot

Elphinstone, Kevin; Klein, Gerwin; Derrin, Philip; Roscoe, Timothy; Heiser, Gernot


2007-05-09


Conference Material


Hot Topics in Operating Systems


San Diego, CA, USA


6


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.


USENIX


seL4, microkernel, verification


http://www.usenix.org/events/hotos07/tech/


nicta:1157


Elphinstone, Kevin; Klein, Gerwin; Derrin, Philip; Roscoe, Timothy; Heiser, Gernot. Towards a Practical, Verified Kernel. In: Galen Hunt Editor, editor/s. Hot Topics in Operating Systems; San Diego, CA, USA. USENIX; 2007-05-09. 6.



Loading citation data...

Citation counts
(Requires subscription to view)