Abstract
The L4.verified project has produced a formal, machine- checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This paper briefly summarises the proof, its main implications and assumptions, reports on the experience in conducting such a large-scale verification, and finally lays out a vision how this formally verified kernel may be used for gaining formal, code-level assurance about safety and security properties of systems on the order of a million lines of code. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Klein, G. (2010). From a verified kernel towards verified systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6461 LNCS, pp. 21–33). https://doi.org/10.1007/978-3-642-17164-2_3
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
