Formal verification of a realistic compiler
Top Cited Papers
- 1 July 2009
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Communications of the ACM
- Vol. 52 (7), 107-115
- https://doi.org/10.1145/1538788.1538814
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.Keywords
Funding Information
- Agence Nationale de la Recherche (ANR-05-SSIA-0019)
This publication has 13 references indexed in Scilit:
- Extraction in Coq: An OverviewPublished by Springer Science and Business Media LLC ,2008
- Formal Verification of a C-like Memory Model and Its Uses for Verifying Program TransformationsJournal of Automated Reasoning, 2008
- Formal verification of translation validatorsPublished by Association for Computing Machinery (ACM) ,2008
- Formal certification of a compiler back-end orPublished by Association for Computing Machinery (ACM) ,2006
- Formal Verification of a C Compiler Front-EndLecture Notes in Computer Science, 2006
- Compiler verificationACM SIGSOFT Software Engineering Notes, 2003
- Translation validation for an optimizing compilerPublished by Association for Computing Machinery (ACM) ,2000
- From system F to typed assembly languageACM Transactions on Programming Languages and Systems, 1999
- Iterated register coalescingACM Transactions on Programming Languages and Systems, 1996
- Register allocation & spilling via graph coloringPublished by Association for Computing Machinery (ACM) ,1982