Sciweavers

Share
POPL
2006
ACM

Formal certification of a compiler back-end or: programming a compiler with a proof assistant

9 years 9 months ago
Formal certification of a compiler back-end or: programming a compiler with a proof assistant
This paper reports on the development and formal certification (proof of semantic preservation) of a compiler from Cminor (a Clike imperative language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a certified compiler is useful in the context of formal methods applied to the certification of critical software: the certification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well. Categories and Subject Descriptors F.3.1 [Logics and meanings of programs]: Specifying and verifying and reasoning about programs--Mechanical verification.; D.2.4 [Software engineering]: Software/program verification--Correctness proofs, formal methods, reliability; D.3.4 [Programming languages]: Processors--Compilers, optimization General Terms Languages, Reliability, Security, Verification. Keywords Certified compilation, semantic preservation, program ...
Xavier Leroy
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2006
Where POPL
Authors Xavier Leroy
Comments (0)
books