Formalising the L4 microkernel API

This paper gives an overview of a pilot project on the specification and verification of the L4 highperformance microkernel. Of the three aspects examined in the project, we describe one in more detail: the formalisation of the kernel's Application Programming Interface using the B Method. We conclude that machine-supported formal verification of software is at a turning point; that it is now feasible, and desirable, to formally verify production-quality operating systems.

• Type: Conference
• Year: 2006
• Where: CATS
• Authors: Rafal Kolanski, Gerwin Klein
• Keywords: CATS 2006, CATS 2007, Kernel's Application Programming, Machine-supported Formal Verification, Production-quality Operating Systems