A formally-verified C static analyzer

Abstract : This paper reports on the design and soundness proof, using the Coq proof assistant, of Verasco, a static analyzer based on abstract interpretation for most of the ISO C 1999 language (excluding re-cursion and dynamic allocation). Verasco establishes the absence of run-time errors in the analyzed programs. It enjoys a modular architecture that supports the extensible combination of multiple abstract domains, both relational and non-relational. Verasco integrates with the CompCert formally-verified C compiler so that not only the soundness of the analysis results is guaranteed with math-ematical certitude, but also the fact that these guarantees carry over to the compiled code.
Type de document :
Communication dans un congrès
POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. ACM, pp.247-259, 〈10.1145/2676726.2676966〉
Liste complète des métadonnées

Littérature citée [36 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01078386
Contributeur : Xavier Leroy <>
Soumis le : mardi 28 octobre 2014 - 19:17:11
Dernière modification le : vendredi 17 février 2017 - 16:11:21
Document(s) archivé(s) le : vendredi 14 avril 2017 - 11:34:24

Fichier

verasco-popl2015.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, David Pichardie. A formally-verified C static analyzer. POPL 2015: 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2015, Mumbai, India. ACM, pp.247-259, 〈10.1145/2676726.2676966〉. 〈hal-01078386〉

Partager

Métriques

Consultations de
la notice

702

Téléchargements du document

253