The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Translation validation for a verified OS kernel
The work
| Authors | Thomas Arthur Leck Sewell; Magnus O. Myreen; Gerwin Klein |
|---|---|
| Editors | |
| Type | misc |
| Year | 2013 |
| Citekey | sewell2013translation |
Where it appeared
| Published in | Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation |
|---|---|
| Pages | 471--482 |
Identifiers
| DOI | 10.1145/2491956.2462183 |
|---|---|
| OpenAlex | W2126823808 |
Access
| Landing page | https://doi.org/10.1145/2491956.2462183 |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
We extend the existing formal verification of the seL4 operating system microkernel from 9500 lines of C source code to the binary level. We handle all functions that were part of the previous verification. Like the original verification, we currently omit the assembly routines and volatile accesses used to control system hardware.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-25 20:34 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@misc{sewell2013translation,
title = {Translation validation for a verified OS kernel},
author = {Thomas Arthur Leck Sewell and Magnus O. Myreen and Gerwin Klein},
year = {2013},
journal = {Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation},
pages = {471--482},
doi = {10.1145/2491956.2462183},
}
This record lives at https://refs.drheap.org/sewell2013translation/ and will keep doing so.