Check out the new USENIX Web site.

USENIX Home . About USENIX . Events . membership . Publications . Students
HotOS X, Tenth Workshop on Hot Topics in Operating Systems — Abstract

OS Verification—Now!

Harvey Tuch, Gerwin Klein, and Gernot Heiser, National ICT Australia

Abstract

Hard, machine-supported formal verification of software is at a turning point. Recent years have seen theorem proving tools maturing with a number of successful, real-life applications. At the same time, small high-performance OS kernels, which can drastically reduce the size of the trusted computing base, have become more popular. We argue that the combination of those two trends makes it feasible, and desirable, to formally verify production-quality operating systems -- now.
  • View the full text of this paper in HTML and PDF.
    Click here if you have forgotten your password Until June 2006, you will need your USENIX membership identification in order to access the full papers. The Proceedings are published as a collective work, © 2005 by the USENIX Association. All Rights Reserved. Rights to individual papers remain with the author or the author's employer. Permission is granted for the noncommercial reproduction of the complete work for educational or research purposes. USENIX acknowledges all trademarks within this paper.

  • If you need the latest Adobe Acrobat Reader, you can download it from Adobe's site.
To become a USENIX Member, please see our Membership Information.

?Need help? Use our Contacts page.

Last changed: 17 Sept. 2005 aw
HotOS X Final Program
HotOS X Home
USENIX home