The University of New South Wales

Can truly dependable systems be affordable?


Gernot Heiser




With the formal verification of the seL4 microkernel, and subsequent work on assuring its safety and security properties, NICTA has recently not only demonstrated that unprecedented levels of assurance are possible, but also that the cost is competitive. In this talk I will examine what has been achieved, what the cost was, and how this might apply to larger systems, in particular the feasibility of assuring full-system safety or security. The result is cause for optimism.

BibTeX Entry

    booktitle        = {Asia-Pacific Workshop on Systems (APSys)},
    note             = {Keynote at APSys'13},
    month            = jul,
    paperurl         = {},
    slides           = {},
    year             = {2013},
    keywords         = {sel4 microkernel verification},
    title            = {Can Truly Dependable Systems Be Affordable?},
    author           = {Heiser, Gernot},
    address          = {Singapore}