articleCommunications of the ACMJun 30, 2009Closed access

Formal verification of a realistic compiler

XLXavier Leroy

Institut national de recherche en sciences et technologies du numérique

Indexed incrossref

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.

Citation impact

1,114
total citations
FWCI
51.61
Percentile
100%
References
22
Citations per year

Authors

1

Topics & keywords

Topics
Keywords
  • Computer science
  • Programming language
  • Compiler
  • Compiler correctness
  • Executable
  • Compiler construction
  • Correctness
  • Formal verification
No related works found for this paper.

Funding