seL4: formal verification of an OS kernel

SOSP, pp. 207-220, 2009.

Cited by: 1828|Views250
EI
Weibo:
We have shown that full, rigorous, formal verification is practically achievable for operating system microkernels with very reasonable effort compared to traditional development methods

Abstract:

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

Code:

Data:

0
Your rating :
0

 

Best Paper
Best Paper of SOSP, 2009
Tags
Comments