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 two ongoing larger-scale verification projects in more detail.
The paper is written for a technical, non-expert engineering audience.
@article{Klein_09,
author={Gerwin Klein},
title={Operating System Verification --- An Overview},
journal={S\={a}dhan\={a}},
publisher={Springer},
year=2009,
volume=34,
number=1,
month=Feb,
pages={27--69},
}
@techreport{Klein_08-tr,
author={Gerwin Klein},
title={Operating System Verification --- An Overview},
number={NRL-955},
institution={NICTA},
address={Sydney, Australia},
month=jun,
year=2008
}