seL4: formal verification of an OS kernel
SOSP, pp. 207-220, 2009.
We have shown that full, rigorous, formal verification is practically achievable for operating system microkernels with very reasonable effort compared to traditional development methods
Complete formal verification is the only known way to guarantee that a system is free of programming errors. We present our experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. We assume correctness of compiler, assembly code, and hardware, a...More
PPT (Upload PPT)
Best Paper of SOSP, 2009