Certified Static Analysis by Abstract Interpretation

Frédéric Besson 1 David Cachera 1 Thomas Jensen 1 David Pichardie 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : A certified static analysis is an analysis whose semantic validity has been formally proved correct with a proof assistant. We propose a tutorial on building a certified static analysis in Coq. We study a simple bytecode language for which we propose an interval analysis that allows to verify statically that no array-out-of-bounds accesses will occur.
Type de document :
Communication dans un congrès
Foundations of Security Analysis and Design V (FOSAD), 2009, Bertinoro, Italy. Springer-Verlag, 5705, pp.223-257, 2009, Lecture Notes in Computer Science
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00538753
Contributeur : David Pichardie <>
Soumis le : mardi 23 novembre 2010 - 15:10:29
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 16:35:17

Fichier

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

Identifiants

  • HAL Id : inria-00538753, version 1

Citation

Frédéric Besson, David Cachera, Thomas Jensen, David Pichardie. Certified Static Analysis by Abstract Interpretation. Foundations of Security Analysis and Design V (FOSAD), 2009, Bertinoro, Italy. Springer-Verlag, 5705, pp.223-257, 2009, Lecture Notes in Computer Science. 〈inria-00538753〉

Partager

Métriques

Consultations de la notice

404

Téléchargements de fichiers

147