To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 29/11/07 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
                    http://pauillac.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
               Salle 0C8, 175 rue du Chevaleret, 75013 Paris

                          Jeudi 29 novembre, 14h30

                             -----------------
                             Yann Régis-Gianas
                             -----------------

                                   INRIA

                ============================================
                     Des types aux assertions logiques:
                preuve automatique ou assistée de propriétés
                      sur les programmes fonctionnels
                ============================================


J'ai le plaisir de vous inviter à la soutenance de ma thèse de doctorat
effectuée sous l'égide de François Pottier au sein du projet Gallium de
l'INRIA Rocquencourt.

La soutenance se déroulera le jeudi 29 novembre 2007, à 14h30 dans la salle
OC8, au rez-de-chaussée du 175, rue du Chevaleret, dans le 13e arrondissement
de Paris.

Voici un lien pour vous y rendre :

http://maps.google.fr/maps?f=q&hl=fr&geocode=&time=&date=&ttype=&q=175,+rue+du+Chevaleret+75013+paris&sll=47.15984,2.988281&sspn=10.653438,20.566406&ie=UTF8&z=16&iwloc=addr&om=1&iwstate1=actions

Cette thèse étudie deux approches fondées sur l'analyse statique pour
augmenter la sûreté de fonctionnement des programmes informatiques.

La première approche est le typage, qui permet de prouver automatiquement
qu'un programme s'évalue sans échouer. Le langage fonctionnel ML possède un
système de type très riche et un algorithme effectuant une synthèse
automatique de ces types. On s'intéresse à l'adaptation de cet algorithme
pour traiter les types algébriques généralisés (GADT), une forme restreinte
des inductifs de Coq, qui ont été introduits par Hongwei Xi en 2003.

Dans ce cadre, le calcul efficace d'un type plus général est impossible. On
propose une stratification qui maintient les caractéristiques habituelles sur
le fragment ML et qui isole le traitement des GADT en explicitant leur
utilisation.  Le langage obtenu, MLGX, nécessite des annotations de type qui
alourdissent les programmes. Une seconde strate, MLGI, offre au programmeur un
mécanisme de synthèse locale, prédictible et efficace bien qu'incomplet, de la
plupart de ces annotations. Cette première partie s'achève avec une
démonstration de l'expressivité des GADT pour coder les invariants des
automates à pile utilisés par l'analyse syntaxique LR.

Coder des propriétés à l'aide de types permet de transformer le vérificateur
des types en un prouveur automatique. Cependant, la syntaxe des types est
limitée et ne permet pas d'exprimer des propriétés très complexes.  La seconde
approche augmente donc le langage de programmation par des assertions logiques
permettant d'exprimer des spécifications de complexité arbitraire dans la
logique d'ordre supérieur polymorphiquement typée. On vérifie statiquement la
conformité de la sémantique du programme vis-à-vis de ces spécifications à
l'aide d'une technique appelée logique de Hoare qui consiste à engendrer un
ensemble d'obligations de preuves à partir d'un programme annoté.  Une fois
ces obligations de preuve traitées (manuellement à l'aide d'un assistant de
preuve comme Coq ou automatiquement à l'aide d'un prouveur automatique comme
Ergo, si un programme est utilisé correctement et si il renvoie une valeur
alors on est certain que celle-ci respecte les spécifications écrites par le
programmeur.

Habituellement, cette technique est employée sur les langages impératifs. Avec
un langage fonctionnel pur, les problèmes liés à l'état de la mémoire
s'évanouissent tandis que l'ordre supérieur et le polymorphisme en posent de
nouveaux. Nos choix de conception cherchent à maximiser les opportunités
d'utilisation de prouveurs automatiques en traduisant minutieusement les
objets d'ordre supérieur en objets du premier ordre.  Une implantation
prototype du système fournit une illustration de son efficacité dans la preuve
presque totalement automatique d'un module O'Caml d'arbres équilibrés dénotant
des ensembles finis.