Email Gateway (Aug 18 2022 at 13:11): Email Gateway (Aug 18 2022 at 13:11):From: Gerwin Klein <gerwin.klein@nicta.com.au>
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
Last updated: May 03 2024 at 04:19 UTC