Formal verification of a static analyzer: abstract interpretation in type theory

Abstract : This invited talk describes the logical foundations and the status of the ongoing Verasco project, whose aim is to formalize and prove sound a static analyzer for the C programming language based on abstract interpretation, using the Coq proof assistant. (Joint work with David Pichardie, Sandrine Blazy, Jacques-Henri Jourdan, and Vincent Laporte.)
Type de document :
Communication dans un congrès
Types - The 2014 Types Meeting, May 2014, Paris, France. 2014
Liste complète des métadonnées


https://hal.inria.fr/hal-00983847
Contributeur : Xavier Leroy <>
Soumis le : vendredi 25 avril 2014 - 19:18:32
Dernière modification le : lundi 5 octobre 2015 - 16:57:02
Document(s) archivé(s) le : vendredi 25 juillet 2014 - 12:30:21

Fichier

invited-2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00983847, version 1

Collections

Citation

Xavier Leroy. Formal verification of a static analyzer: abstract interpretation in type theory. Types - The 2014 Types Meeting, May 2014, Paris, France. 2014. <hal-00983847>

Partager

Métriques

Consultations de
la notice

266

Téléchargements du document

112