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