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

DOI

10.1145/1538788.1538814

Link

https://doi.org/10.1145/1538788.1538814

Cited from

computer_science, mathematics

Cited by

3 citations across 3 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
• 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.

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

Verification

This reference passed the adversarial substantiation pipeline: it was checked to exist and to support the claim it is attached to. See how references were verified.

Registry ID ref:d840fb800973 · see in the full table