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 ...

• Type: Conference
• Year: 2006
• Where: POPL
• Authors: Xavier Leroy
• Keywords: Clike Imperative Language, Optimization General Terms, POPL 2006, Programming Languages, Software/program Verification--Correctness Proofs