[isabelle] Overview article on OS verification



I'm pleased to announce that the following overview article now has
appeared in Sadhana, vol. 34(1):


Operating System Verification -- An Overview

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

The article is written for a general engineering audience, but it will also be interesting to people closer to formal verification.

Available from:
http://www.ias.ac.in/sadhana
http://www.ias.ac.in/sadhana/CurrentIssueFeb2009.htm

Needless to say, Isabelle plays a prominent role in OS verification these days.

Cheers,
Gerwin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.