Operating system verification—An overview

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...

Full description

Saved in:
Bibliographic Details
Published in:Sadhana (Bangalore) 2009-02, Vol.34 (1), p.27-69
Main Author: Klein, Gerwin
Format: Article
Language:English
Subjects:
Engineering
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 specific ongoing larger-scale verification projects in more detail.
ISSN:0256-2499
0973-7677
DOI:10.1007/s12046-009-0002-4