[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

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:

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


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