A formally verified compiler back-end

Xavier Leroy 1, 2, *
Abstract : This article describes the development and formal verification (proof of semantic preservation) of a compiler back-end from Cminor (a simple imperative intermediate 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 formal methods applied to the certification of critical software: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.
Complete list of metadatas

https://hal.inria.fr/inria-00360768
Contributor : Xavier Leroy <>
Submitted on : Wednesday, February 11, 2009 - 7:40:19 PM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Long-term archiving on : Tuesday, June 8, 2010 - 10:17:00 PM

Files

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00360768, version 1
  • ARXIV : 0902.2137

Citation

Xavier Leroy. A formally verified compiler back-end. 2009. ⟨inria-00360768v1⟩

Share

Metrics

Record views

21

Files downloads

54