Formal Verification of a Realistic Compiler.

Leroy, X. (2009). Formal Verification of a Realistic Compiler. Communications of the ACM, 52(7), 107-115.

Type

Journal article

Intellectual base

Primary research

Year

2009

Volume

52

Issue

7

Pages

107-115

DOI

10.1145/1538788.1538814

DOI registrant

Association for Computing Machinery

Link

https://doi.org/10.1145/1538788.1538814

Cited from

computer_science, mathematics

Cited by

4 citations across 4 artifacts.

Each citation links to the sentence it supports in the citing article.

Primes

• Mathematical Induction
  • preservation-and-progress); compiler correctness via simulation proofs by induction on execution steps (CompCert

    SupportedVerified against the work's full text

    Leroy states that CompCert proves semantic preservation by simulation diagrams and by induction on the execution of the source program.

    “since the proof can proceed by induction on the execution of S. This is the approach that we take in this work.”

    Read by an automated reader; not a human review. How support was checked

• Operationalization
  • The correctness contract is semantics preservation: the compiled program must produce the same observable behaviour the source specifies, up to declared exceptions (undefined behaviour, floating-point rounding) — and "does this object code satisfy this source program?" is a genuine, answerable question, addressed by testing, formal verification, or a proof of compiler correctness.

    This sourcePresents CompCert, a machine-checked proof of semantics preservation — the correctness contract relating compiled code to source.

    SupportedVerified against the work's full text

    Leroy defines compiler correctness as preservation of observable behaviours, relaxed for undefined ('going wrong') behaviours, and covers testing, validation and proof.

    “Consider a source program S and a compiled program C produced by a compiler. Our aim is to prove that the seman- tics of S was preserved during compilation.”

    Read by an automated reader; not a human review. How support was checked

• Well-Foundedness (Well-Ordering)
  • Listed in the references but not attached to a specific claim.

Domain-specific

• Formal Verification
  • CompCert, the verified optimizing C compiler developed by Xavier Leroy and collaborators

    This sourceLeroy's account of CompCert, a formally verified, lightly optimizing C compiler whose semantic-preservation proof is machine-checked in Coq.

    SupportedVerified against the source

    Read by an automated reader; not a human review. How support was checked

Verification

Does it exist? Confirmed. This work's DOI resolves to a registered record, which fixes its identity. That is all it fixes.

Does it back the claim? Read against the text for 3 of 4 citations: 3 supported. Each verdict is shown under its citation below, with what in the work backs the sentence.

Support is checked per citation rather than per work — the same source can be cited soundly in one article and wrongly in another. Per-citation recording began recently, so a citation with no recorded check is a gap in the record rather than evidence it went unchecked.

See how references were verified.

Registry ID ref:d840fb800973 · see in the full table