Comprehensive formal verification of an OS microkernel

ACM Trans. Comput. Syst., 2014.

Cited by: 232|Bibtex|Views56|DOI:https://doi.org/10.1145/2560537
EI
Other Links: dl.acm.org|dblp.uni-trier.de|academic.microsoft.com

Abstract:

We present an in-depth coverage of the comprehensive machine-checked formal verification of seL4, a general-purpose operating system microkernel. We discuss the kernel design we used to make its verification tractable. We then describe the functional correctness proof of the kernel's C implementation and we cover further steps that transf...More

Code:

Data:

Your rating :
0

 

Tags
Comments