Abstract
We report on the first formal pervasive verification of an operating system microkernel featuring the correctness of inline assembly, large non-trivial C portions, and concurrent devices in a single seamless formal proof. We integrated all relevant verification results we had achieved so far [21,20,2,5,4] into a single top-level theorem of microkernel correctness. This theorem states the simulation of user processes with own, separate virtual memories - via the microkernel - by the underlying hardware with devices. All models, theorems, and proofs are formalized in the interactive proof system Isabelle/HOL. © 2010 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Alkassar, E., Paul, W. J., Starostin, A., & Tsyban, A. (2010). Pervasive verification of an OS microkernel: Inline assembly, memory consumption, concurrent devices. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6217 LNCS, pp. 71–85). https://doi.org/10.1007/978-3-642-15057-9_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
