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.
Type de document :
Communication dans un congrès
Dimitra Giannakopoulou and Gwen Salaün. SEFM 2014 - 12th International Conference Software Engineering and Formal Methods, Sep 2014, Grenoble, France. Springer, 8702, pp.1-4, 2014, Lecture Notes in Computer Science. <10.1007/978-3-319-10431-7_1>
Liste complète des métadonnées


https://hal.inria.fr/hal-01059423
Contributeur : Xavier Leroy <>
Soumis le : dimanche 31 août 2014 - 18:41:02
Dernière modification le : mercredi 14 décembre 2016 - 01:07:56
Document(s) archivé(s) le : lundi 1 décembre 2014 - 11:41:14

Fichier

abstract.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Xavier Leroy. Formal proofs of code generation and verification tools. Dimitra Giannakopoulou and Gwen Salaün. SEFM 2014 - 12th International Conference Software Engineering and Formal Methods, Sep 2014, Grenoble, France. Springer, 8702, pp.1-4, 2014, Lecture Notes in Computer Science. <10.1007/978-3-319-10431-7_1>. <hal-01059423>

Partager

Métriques

Consultations de
la notice

159

Téléchargements du document

190