Open AccessOperating system verification—An overview
Author(s) -
Gerwin Klein
Publication year - 2009
Publication title -
sadhana
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.268
H-Index - 49
eISSN - 0973-7677
pISSN - 0256-2499
DOI - 10.1007/s12046-009-0002-4
Subject(s) - computer science , software verification , verification , programming language , formal verification , mathematical proof , software engineering , code (set theory) , functional verification , runtime verification , verification and validation , software , intelligent verification , formal methods , software system , software construction , engineering , mathematics , operations management , geometry , set (abstract data type)
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.
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom