Comprehensive Formal Verification of an OS Microkernel
Comprehensive Formal Verification of an OS Microkernel
About this item
Full title
Author / Creator
Publisher
New York, NY: Association for Computing Machinery
Journal title
Language
English
Formats
Publication information
Publisher
New York, NY: Association for Computing Machinery
Subjects
More information
Scope and Contents
Contents
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 transform thi...
Alternative Titles
Full title
Comprehensive Formal Verification of an OS Microkernel
Authors, Artists and Contributors
Identifiers
Primary Identifiers
Record Identifier
TN_cdi_proquest_miscellaneous_1520939037
Permalink
https://devfeature-collection.sl.nsw.gov.au/record/TN_cdi_proquest_miscellaneous_1520939037
Other Identifiers
ISSN
0734-2071
E-ISSN
1557-7333
DOI
10.1145/2560537
