Xavier Leroy presents the formal verification of CompCert, a compiler from Clight (a subset of C) to PowerPC assembly code, using the Coq proof assistant. The goal is to ensure that the generated code preserves the semantics of the source program. CompCert is a realistic compiler that compiles a large subset of C, produces efficient code for embedded systems, and is verified through formal methods. The verification involves proving that the compiler's transformations preserve the semantics of the source code, ensuring that the generated code behaves as intended. The compiler is structured into multiple passes, each of which is formally verified. The verification process includes defining formal semantics for the source and target languages, proving that each transformation step preserves semantics, and using Coq to mechanize these proofs. The CompCert compiler is verified to preserve the safety properties of the source code, ensuring that the generated code is correct. The verification process involves proving that the compiler's transformations are correct, using a combination of formal methods and automated proof techniques. The paper discusses the challenges of verifying compilers, the importance of formal verification in safety-critical software, and the techniques used to verify CompCert. The verification of CompCert demonstrates that it is possible to formally verify a realistic compiler, ensuring that the generated code is correct and safe. The paper concludes that formal verification is a promising approach for ensuring the correctness of compilers, and that CompCert provides a successful example of this approach.Xavier Leroy presents the formal verification of CompCert, a compiler from Clight (a subset of C) to PowerPC assembly code, using the Coq proof assistant. The goal is to ensure that the generated code preserves the semantics of the source program. CompCert is a realistic compiler that compiles a large subset of C, produces efficient code for embedded systems, and is verified through formal methods. The verification involves proving that the compiler's transformations preserve the semantics of the source code, ensuring that the generated code behaves as intended. The compiler is structured into multiple passes, each of which is formally verified. The verification process includes defining formal semantics for the source and target languages, proving that each transformation step preserves semantics, and using Coq to mechanize these proofs. The CompCert compiler is verified to preserve the safety properties of the source code, ensuring that the generated code is correct. The verification process involves proving that the compiler's transformations are correct, using a combination of formal methods and automated proof techniques. The paper discusses the challenges of verifying compilers, the importance of formal verification in safety-critical software, and the techniques used to verify CompCert. The verification of CompCert demonstrates that it is possible to formally verify a realistic compiler, ensuring that the generated code is correct and safe. The paper concludes that formal verification is a promising approach for ensuring the correctness of compilers, and that CompCert provides a successful example of this approach.