Formal Verification of a C Value Analysis Based on Abstract Interpretation

Résumé : Les analyseurs statiques fondés sur l'interprétation abstraite sont des logiciels complexes implémentant des algorithmes sophistiqués. Bien que es techniques d'analyse statique soient bien comprises, leur implémentation pour de vrais langages est toujours source d'erreurs. Cet article présente une vérification formelle à l'aide de l'assistant à la preuve Coq : une formalisation d'une analyse de valeurs (fondée sur m'interprétation abstraite), et une preuve de correction de l'analyse de valeurs. La formalisation repose sur des interfaces génériques. La preuve mécanisée est facilitée par une validation a posteriori d'un itérateur de point fixe à la Bourdoncle. Ce travail a été intégré au compilateur formellement vérifié CompCert C. Notre analyse vérifiée opère directement sur un langage intermédiaire du compilateur ayant le même pouvoir d'expression que C. L'extraction automatique de notre analyse de valeurs en OCaml fournit un programme dont les résultats sont compétitifs avec ceux fournis par l'outil Frama-C.
Type de document :
Communication dans un congrès
Manuel Fahndrich and Francesco Logozzo. SAS - 20th Static Analysis Symposium, Jun 2013, Seattle, United States. Springer, Lecture Notes in Computer Science, pp.324-344, 2013, 7935
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00812515
Contributeur : Sandrine Blazy <>
Soumis le : vendredi 12 avril 2013 - 11:46:33
Dernière modification le : jeudi 15 novembre 2018 - 11:57:40
Document(s) archivé(s) le : lundi 3 avril 2017 - 04:36:42

Fichiers

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

Identifiants

  • HAL Id : hal-00812515, version 1
  • ARXIV : 1304.3596

Citation

Sandrine Blazy, Vincent Laporte, André Maroneze, David Pichardie. Formal Verification of a C Value Analysis Based on Abstract Interpretation. Manuel Fahndrich and Francesco Logozzo. SAS - 20th Static Analysis Symposium, Jun 2013, Seattle, United States. Springer, Lecture Notes in Computer Science, pp.324-344, 2013, 7935. 〈hal-00812515〉

Partager

Métriques

Consultations de la notice

1056

Téléchargements de fichiers

228