Sciweavers

Share
HOTOS
2007
IEEE

Towards a Practical, Verified Kernel

10 years 5 months ago
Towards a Practical, Verified Kernel
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.
Kevin Elphinstone, Gerwin Klein, Philip Derrin, Ti
Added 16 Aug 2010
Updated 16 Aug 2010
Type Conference
Year 2007
Where HOTOS
Authors Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe, Gernot Heiser
Comments (0)
books