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.

• Type: Conference
• Year: 2007
• Where: HOTOS
• Authors: Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe, Gernot Heiser
• Keywords: Formal Methods Practitioners, HOTOS 2007, Iterative Development Methodology, Operating System, Operating System Kernel