Skip to main content

Operating system verification — an overview


Gerwin Klein



Invited paper. Journal homepage.


This paper gives a high-level introduction to the topic of formal, interactive, machine-checked software verification in general, and the verification of operating systems code in particular. We survey the state of the art, the advantages and limitations of machine-checked code proofs, and describe one specific ongoing larger-scale verification project in more detail.

BibTeX Entry

    author           = {Klein, Gerwin},
    number           = {1},
    month            = feb,
    year             = {2009},
    keywords         = {formal software verification, operating systems, theorem proving},
    title            = {Operating System Verification --- An Overview},
    volume           = {34},
    pages            = {26--69},
    journal          = {Sadhana},
    paperurl         = {}


Served by Apache on Linux on seL4.