NICTA
UNSW
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.
@article{Klein_09, month = feb, journal = {Sadhana}, paperurl = {https://trustworthy.systems/publications/nicta_full_text/955.pdf}, year = {2009}, keywords = {formal software verification, operating systems, theorem proving}, title = {Operating System Verification --- An Overview}, volume = {34}, number = {1}, author = {Klein, Gerwin}, pages = {26--69} }