Formal verification of a realistic compiler
The work
| Authors | Xavier Leroy |
|---|---|
| Editors | |
| Type | article |
| Year | 2009 |
| Citekey | leroy2009formal |
Where it appeared
| Published in | Communications of the ACM |
|---|---|
| Publisher | Association for Computing Machinery |
| Volume | 52 |
| Issue | 7 |
| Pages | 107--115 |
Identifiers
| DOI | 10.1145/1538788.1538814 |
|---|---|
| OpenAlex | W2023035194 |
Access
| Landing page | https://doi.org/10.1145/1538788.1538814 |
|---|
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
This paper reports on the development and formal verification (proof of semantic preservation) of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of critical software and its formal verification: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-25 13:36 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{leroy2009formal,
title = {Formal verification of a realistic compiler},
author = {Xavier Leroy},
year = {2009},
journal = {Communications of the ACM},
publisher = {Association for Computing Machinery},
volume = {52},
number = {7},
pages = {107--115},
doi = {10.1145/1538788.1538814},
}
This record lives at https://refs.drheap.org/leroy2009formal/ and will keep doing so.