Programmation d'un interpréteur abstrait certifié en logique constructive.

A static analyzer aims at automatically deducing program pr operties by examining its source code. Proving the correctness of an analyzer is ba sed on semantic properties, and becomes difficult to ensure when complex analysis technique s are involved. We propose to adapt the general theory of static analysis by abstract interpret ation to the framework of constructive logic. Implementing this formalism into the Coq proof assis tant then allows for automatic extraction of certified analyzers. We focus here on a simple i mperative language and present the computation of fixpoints by widening/narrowing and synt ax-directed iteration techniques. MOTS-CLES :Analyse statique, interpretation abstraite, calcul de poi nt fixe, logique constructive, assistant de preuve