Structural abstract interpretation, A formal study using Coq - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2008

Structural abstract interpretation, A formal study using Coq

Yves Bertot

Résumé

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.
Fichier principal
Vignette du fichier
absint.pdf (317.32 Ko) Télécharger le fichier
README (93 B) Télécharger le fichier
absint.v (49.19 Ko) Télécharger le fichier
absint81.v (49.47 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Format : Autre
Format : Autre
Format : Autre

Dates et versions

inria-00329572 , version 1 (13-10-2008)
inria-00329572 , version 2 (20-10-2008)

Identifiants

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

Citer

Yves Bertot. Structural abstract interpretation, A formal study using Coq. LERNET Summer School, Ana Bove and Jorge Sousa Pinto, Feb 2008, Piriapolis, Uruguay. ⟨inria-00329572v2⟩

Collections

INRIA INRIA2 ANR
1129 Consultations
1405 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More