Back to Search
Start Over
Formal Verification of a Realistic Compiler.
- Source :
- Communications of the ACM; Jul2009, Vol. 52 Issue 7, p107-115, 9p, 2 Diagrams, 1 Graph
- Publication Year :
- 2009
-
Abstract
- This paper reports on the development and formal verification (proof of semantic preservation) of Comp Cert, 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. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 00010782
- Volume :
- 52
- Issue :
- 7
- Database :
- Complementary Index
- Journal :
- Communications of the ACM
- Publication Type :
- Periodical
- Accession number :
- 43019159
- Full Text :
- https://doi.org/10.1145/1538788.1538814