Structural abstract interpretation, A formal study using Coq

Yves Bertot 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Abstract interpreters are tools to compute approximations for behaviors of a program. These approximations can then be used for optimisation or for error detection. In this paper, we show how to describe an abstract interpreter using the type-theory based theorem prover Coq, using inductive types for syntax and structural recursive programming for the abstract interpreter's kernel. The abstract interpreter can then be proved correct with respect to a Hoare logic for the programming language.
Type de document :
Communication dans un congrès
Ana Bove and Jorge Sousa Pinto. LERNET Summer School, Feb 2008, Piriapolis, Uruguay. Springer, 2008, Lecture Notes in Computer Science


https://hal.inria.fr/inria-00329572
Contributeur : Yves Bertot <>
Soumis le : lundi 20 octobre 2008 - 16:17:06
Dernière modification le : lundi 5 octobre 2015 - 17:01:41
Document(s) archivé(s) le : mardi 21 septembre 2010 - 17:32:20

Fichiers

Identifiants

  • HAL Id : inria-00329572, version 2
  • ARXIV : 0810.2179

Collections

Citation

Yves Bertot. Structural abstract interpretation, A formal study using Coq. Ana Bove and Jorge Sousa Pinto. LERNET Summer School, Feb 2008, Piriapolis, Uruguay. Springer, 2008, Lecture Notes in Computer Science. <inria-00329572v2>

Partager

Métriques

Consultations de
la notice

892

Téléchargements du document

537