Comparing Techniques for Certified Static Analysis

David Cachera 1 David Pichardie 1
1 CELTIQUE - Software certification with semantic analysis
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
Abstract : A certified static analysis is an analysis whose semantic validity has been formally proved correct with a proof assistant. The recent increasing interest in using proof assistants for mechanizing programming language metatheory has given rise to several approaches for certification of static analysis. We propose a panorama of these techniques and compare their respective strengths and weaknesses.
Type de document :
Communication dans un congrès
The NASA Formal Methods Symposium (NFM), 2009, Moffett Field, United States. NASA Ames Research Center, pp.111-115, 2009
Liste complète des métadonnées

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

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

Fichier

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

Identifiants

  • HAL Id : inria-00538772, version 1

Citation

David Cachera, David Pichardie. Comparing Techniques for Certified Static Analysis. The NASA Formal Methods Symposium (NFM), 2009, Moffett Field, United States. NASA Ames Research Center, pp.111-115, 2009. 〈inria-00538772〉

Partager

Métriques

Consultations de la notice

378

Téléchargements de fichiers

102