Pervasive Compiler Verification – From Verified Programs to Verified Systems
The work
| Authors | Dirk Leinenbach; Elena Petrova |
|---|---|
| Editors | |
| Type | article |
| Year | 2008 |
| Citekey | leinenbach2008pervasive |
Where it appeared
| Published in | Electronic Notes in Theoretical Computer Science |
|---|---|
| Publisher | Elsevier BV |
| Volume | 217 |
| Pages | 23--40 |
Identifiers
| DOI | 10.1016/j.entcs.2008.06.040 |
|---|---|
| OpenAlex | W2134927133 |
Access
| Landing page | https://doi.org/10.1016/j.entcs.2008.06.040 |
|---|---|
| Free full text | https://www.sciencedirect.com/science/article/pii/S1571066108003836/pdf |
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 report in this paper on the formal verification of a simple compiler for the C-like programming language C0. The compiler correctness proof meets the special requirements of pervasive system verification and allows to transfer correctness properties from the C0 layer to the assembler and hardware layers. The compiler verification is split into two parts: the correctness of the compiling specification (which can be translated to executable ML code via Isabelle's code generator) and the correctness of a C0 implementation of this specification. We also sketch a method to solve the boot strap problem, i.e., how to obtain a trustworthy binary of the C0 compiler from its C0 implementation. Ultimately, this allows to prove pervasively the correctness of compiled C0 programs in the real system.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-25 15:53 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{leinenbach2008pervasive,
title = {Pervasive Compiler Verification – From Verified Programs to Verified Systems},
author = {Dirk Leinenbach and Elena Petrova},
year = {2008},
journal = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier BV},
volume = {217},
pages = {23--40},
doi = {10.1016/j.entcs.2008.06.040},
}
This record lives at https://refs.drheap.org/leinenbach2008pervasive/ and will keep doing so.