Skip to Main content Skip to Navigation
New interface
Conference papers

Formal proofs of code generation and verification tools

Abstract : Tool-assisted verification of critical software has great potential but is limited by two risks: unsoundness of the verification tools, and miscompilation when generating executable code from the sources that were verified. A radical solution to these two risks is the deductive verification of compilers and verification tools themselves. In this invited talk, I describe two ongoing projects along this line: CompCert, a verified C~compiler, and Verasco, a verified static analyzer based on abstract interpretation.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download
Contributor : Xavier Leroy Connect in order to contact the contributor
Submitted on : Sunday, August 31, 2014 - 6:41:02 PM
Last modification on : Thursday, February 3, 2022 - 11:18:23 AM
Long-term archiving on: : Monday, December 1, 2014 - 11:41:14 AM


Files produced by the author(s)




Xavier Leroy. Formal proofs of code generation and verification tools. SEFM 2014 - 12th International Conference Software Engineering and Formal Methods, Sep 2014, Grenoble, France. pp.1-4, ⟨10.1007/978-3-319-10431-7_1⟩. ⟨hal-01059423⟩



Record views


Files downloads