Vérification de programmes à l'aide de formules caractéristiques
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
This dissertation describes a new approach to program verification, based on characteristic formulae the characteristic formula of a program is a higher-order logic formula that describes the behavior of that program, in the sense that it is sound and complete with respect to the semantics. This formula can be exploited in an interactive theorem prover to establish that the program satisfies a specification expressed in the style of separation logic, with respect to total correctness. The characteristic formula of a program is automatically generated from its source code alone. In particular, there is no need to annotate the source code with specifications or loop invariants, as such information can be given in interactive proof scripts. One key feature of characteristic formulae is that they are of linear size and that they can be pretty-printed in a way that closely resemble the source code they describe, even though they do not refer to the syntax of the programming language Characteristic formulae serve as a basis for a tool, called CFML, that supports the verification of CAML programs using the coq proof assistant. CFML has been employed to verify about half of the content of okasaki's book on purely functional data structures, and to verify several imperative data structures such as mutable lists, sparse arrays and union-find. Cfml also supports reasoning on higher-order imperative functions, such as functions in cps form and higher-order iterators.
Abstract FR:
Cette thèse introduit une nouvelle approche a la vérification de programmes, basée sur des formules caractéristiques. La formule caractéristique d'un programme est une formule de la logique d'ordre supérieur qui décrit le comportement d'un programme d'une manière correcte et complète vis-à-vis de la sémantique. Cette formule peut être exploitée dans un assistant de preuve pour établir de manière interactive qu'un programme satisfait une spécification de correction totale exprimée dans le style de la logique de séparation. La formule caractéristique d'un programme est automatiquement générée à partir de son code source il n'est pas nécessaire d'annoter ce code par des spécifications ou des invariants de boucle vu que ces informations peuvent être fournies dans le script de preuve. Un aspect essentiel des formules caractéristiques est qu'elles sont de taille linéaire et qu'elles peuvent être affichées comme le code source qu'elles décrivent, bien qu'elles ne fassent pas référence à la syntaxe du langage de programmation. Ces formules caractéristiques sont au coeur d'un outil, dénomme CFML, qui permet de vérifier des programmes CAML à l'aide de l'assistant de preuve coq. CFML a été utilisé pour vérifier la moitie du contenu du livre de Chris Okasaki sur les structures de données purement fonctionnelles, ainsi que pour vérifier plusieurs structures de données impératives telles que les listes mutables, les tableaux creux, ou encore la structure d'union-find. CFML supporte également le raisonnement sur les fonctions impératives d'ordre supérieur, comme les fonctions en forme CPS ou les itérateurs d'ordre supérieur.