seL4 in Australia: From Research to Real-World Trustworthy Systems
The work
| Title | seL4 in Australia: From Research to Real-World Trustworthy Systems |
|---|---|
| Authors | Gernot Heiser; Gerwin Klein; June Andronick |
| Type | article |
| Year | 2020 |
| Citekey | heiser2020sel4 |
Where it appeared
| Published in | Communications of the ACM |
|---|---|
| Publisher | Association for Computing Machinery |
| Volume | 63 |
| Issue | 4 |
| Pages | 72--75 |
Identifiers
| DOI | 10.1145/3378426 |
|---|---|
| OpenAlex | W3010700826 |
Access
| Landing page | https://doi.org/10.1145/3378426 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1145/3378426 |
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.
Copy held
| Kind | PDF, 494.3 kB |
|---|---|
| Retrieved | 2026-08-10 |
| Held | local, for personal reference |
| Where it came from | https://trustworthy.systems/publications/full_text/Heiser_KA_20.pdf |
Where this came from
| How it got here | already cited · cited in bibtex |
|---|---|
| First seen | 2026-08-10 |
| Record | reviewed by a person |
| Approved | 2026-08-16 |
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},
volume = {63},
number = {4},
pages = {72--75},
publisher = {Association for Computing Machinery},
doi = {10.1145/3378426},
url = {https://dl.acm.org/doi/pdf/10.1145/3378426},
}
This record lives at https://refs.drheap.org/heiser2020sel4/ and will keep doing so.