A Certified Denotational Abstract Interpreter

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 : Abstract Interpretation proposes advanced techniques for static analysis of programs that raise specific challenges for machine-checked soundness proofs. Most classical dataflow analysis techniques iterate operators on lattices without infinite ascending chains. In contrast, abstract interpreters are looking for fixpoints in infinite lattices where widening and narrowing are used for accelerating the convergence. Smart iteration strategies are crucial when using such accelerating operators because they directly impact the precision of the analysis diagnostic. In this paper, we show how we manage to program and prove correct in Coq an abstract interpreter that uses iteration strategies based on program syntax. A key component of the formalization is the introduction of an intermediate semantics based on a generic least-fixpoint operator on complete lattices and allows us to decompose the soundness proof in an elegant manner.
Type de document :
Communication dans un congrès
International Conference on Interactive Theorem Proving (ITP), 2010, Edimburgh, United Kingdom. Springer-Verlag, 6172, pp.9-24, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00537810
Contributeur : David Pichardie <>
Soumis le : vendredi 19 novembre 2010 - 13:57:54
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : vendredi 26 octobre 2012 - 16:01:37

Fichier

main.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • HAL Id : inria-00537810, version 1

Citation

David Cachera, David Pichardie. A Certified Denotational Abstract Interpreter. International Conference on Interactive Theorem Proving (ITP), 2010, Edimburgh, United Kingdom. Springer-Verlag, 6172, pp.9-24, 2010, Lecture Notes in Computer Science. 〈inria-00537810〉

Partager

Métriques

Consultations de la notice

306

Téléchargements de fichiers

134