seL4 in Australia: From Research to Real-World Trustworthy Systems

The work

AuthorsGernot Heiser; Gerwin Klein; June Andronick
Editors
Typearticle
Year2020
Citekeyheiser2020sel4

Where it appeared

Published inCommunications of the ACM
PublisherAssociation for Computing Machinery
Volume63
Issue4
Pages72--75

Identifiers

DOI10.1145/3378426
OpenAlexW3010700826

Access

Landing pagehttps://doi.org/10.1145/3378426
Free full texthttps://dl.acm.org/doi/pdf/10.1145/3378426

Related

Distinct frombowen1993formal
Distinct fromsewell2026escaping

Abstract

The seL4 microkernel was the first operating system proved functionally correct to the source-code level. We provide an overview of its development since, in terms of extending verification, evolving the kernel to support wider classes of real-world systems, discuss some of the frameworks that allow extending verification guarantees to other critical system components, as well as real-world deployments.

A copy is held

pdf, 482.7 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereimport via bibtex
Added2026-08-10 00:00 UTC
Approved bya person 2026-08-16 15:30 UTC

Filed under

andronick cacm gerwinklein heiser the-copy-is-not-the-work when-software-kills

Cite it as

@article{heiser2020sel4,
  title        = {seL4 in Australia: From Research to Real-World Trustworthy Systems},
  author       = {Gernot Heiser and Gerwin Klein and June Andronick},
  year         = {2020},
  journal      = {Communications of the ACM},
  publisher    = {Association for Computing Machinery},
  volume       = {63},
  number       = {4},
  pages        = {72--75},
  doi          = {10.1145/3378426},
}

This record lives at https://refs.drheap.org/heiser2020sel4/ and will keep doing so.