leroy_formal_2009:
  type: article
  title: Formal verification of a realistic compiler
  author: Leroy, Xavier
  date: 2009-07
  page-range: 107-115
  url:
    value: https://dl.acm.org/doi/10.1145/1538788.1538814
    date: 2024-04-22
  serial-number:
    doi: 10.1145/1538788.1538814
    issn: 0001-0782, 1557-7317
  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.'
  parent:
    type: periodical
    title: Communications of the ACM
    issue: 7
    volume: 52