thesis

Vérification formelle d'un compilateur optimisant pour langages fonctionnels

Defense date:

Jan. 1, 2009

Edit

Institution:

Paris 7

Disciplines:

Computer sciences

Authors:

Directors:

Abstract EN:

As part of formal verification of critical software, preserving properties established on the source code in the executable code seems to be crucial. To have this preservation, the compiler has to be verified itself. A compiler is formally verified if it is joined with a proof of semantic preservation: the behavior of the compiled code preserves the source code behavior. If the compilation succeeds. The CompCert project investigates the formal vérification of realistic compilers usable for critical embedded software. The project designs, develops and mechanically verifies compilers within the Coq Proof Assistant. Using the extraction mechanism of Coq, the compiler is automatically extracted into OCaml code, which is compiled by the Objective Cami System. This thesis deals with the design, development and mechanized verification ,in the Coq Proof Assistant, of a compiler for the purely functional fragment of ML, which is the language of extracted from Coq extraction. Concretely, a front-end from miniML to Cminor has been developed. Cminor is a low-level C-like language, that is the first intermediate language of the CompCert back-end. Such as the source language is expressive, the compiler is realistic. Classical functional language compilation optimizations are done: uncurrying, uniform data structure representation and an optimizing CPS translation. As in modem compiler for high-level languages, the miniML compiler can interact with a memory manager. This interaction has been mechanized verified.

Abstract FR:

Dans le cadre de la vérification de logiciels dans le domaine de l'embarqué critique, la préservation des propriétés établies sur le code source par le code exécutable est un point crucial. Cette préservation est obtenue par la vérification formelle du compilateur. Un compilateur est formellement vérifié s'il est accompagné d'une preuve de préservation sémantique : le comportement du programme source est préservé par celui du programme compilé, si la compilation réussit. Le projet CompCert s'intéresse à la vérification formelle de compilateur réaliste pour l'embarqué critique. Il s'agit de définir, développer et formellement vérifier de tels compilateurs dans l'assistant de preuves Coq. Cette thèse s'intéresse au développement d'un tel compilateur pour le fragment purement fonctionnel de miniML. Plus précisément, il s'agit de la vérification formelle d'une chaîne de compilation en amont de miniML vers Cminor, premier langage intermédiaire de la chaîne de compilation en aval de CompCert. Tout comme le langage source est expressif, la compilation est réaliste. Elle comporte des optimisations classiques de la compilation de langages fonctionnels : décurryfication, représentation uniforme desdonnées et une transformation CPS optimisante. Comme les compilateur moderne pour langages de haut niveau, le code généré interagit avec un gestionnaire de mémoire automatique. Cette interaction a été vérifiée.