ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne
Autres revues >>

Technique et Science Informatiques

0752-4072
Revue des sciences et technologies de l'information
 

 ARTICLE VOL 30/4 - 2011  - pp.381-408  - doi:10.3166/tsi.30.381-408
TITRE
Programmation d´un interpréteur abstrait certifié en logique constructive

TITLE
Programming a certified abstract interpreter in constructive logic

RÉSUMÉ
Un analyseur statique permet de déduire automatiquement des propriétés d’un programme à partir de son code. La preuve de correction d’un analyseur repose sur des propriétés sémantiques, et devient difficile à assurer lorsque l’analyse met en oeuvre des techniques symboliques complexes. Nous proposons une adaptation de la théorie générale de l’analyse statique par interprétation abstraite au cadre de la logique constructive. L’implémentation de ce formalisme dans l’assistant de preuve Coq permet alors d’extraire automatiquement des analyseurs certifiés. Nous nous intéressons plus particulièrement à un langage impératif simple, et présentons en détail le calcul de point fixe par élargissement/rétrécissement et itération dirigée par la syntaxe.


ABSTRACT
A static analyzer aims at automatically deducing program properties by examining its source code. Proving the correctness of an analyzer is based on semantic properties, and becomes difficult to ensure when complex analysis techniques are involved. We propose to adapt the general theory of static analysis by abstract interpretation to the framework of constructive logic. Implementing this formalism into the Coq proof assistant then allows for automatic extraction of certified analyzers. We focus here on a simple imperative language and present the computation of fixpoints by widening/narrowing and syntax-directed iteration techniques.


AUTEUR(S)
David CACHERA, David PICHARDIE

Reçu le 16 février 2009.   

MOTS-CLÉS
analyse statique, interprétation abstraite, calcul de point fixe, logique constructive, assistant de preuve.

KEYWORDS
static analysis, abstract interpretation, fixpoint computation, constructive logic, proof assistant.

LANGUE DE L'ARTICLE
Français

 PRIX
• Abonné (hors accès direct) : 12.5 €
• Non abonné : 25.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (319 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier