OS verification - now!

Download files
Access & Terms of Use
open access
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.
Persistent link to this record
Link to Publisher Version
Author(s)
Tuch, Harvey
Klein, Gerwin
Heiser, Gernot
Supervisor(s)
Creator(s)
Editor(s)
Translator(s)
Curator(s)
Designer(s)
Arranger(s)
Composer(s)
Recordist(s)
Conference Proceedings Editor(s)
Other Contributor(s)
Corporate/Industry Contributor(s)
Publication Year
2005
Resource Type
Conference Paper
Degree Type
UNSW Faculty
Files
download Tuch_KH_05.pdf 98.09 KB Adobe Portable Document Format
Related dataset(s)