Programming a certified abstract interpreter in constructive logic
Programmation d'un interpréteur abstrait certifié en logique constructive
Résumé
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.
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.