To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 02/06/09 - 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 de conférences du bâtiment 7

                            Mardi 2 juin, 10h30

                               --------------
                               Zaynah Dargaye
                               --------------

                              INRIA et ENSIIE

   ======================================================================
   Vérification formelle de l'interaction avec un gestionnaire de mémoire
   ======================================================================

Dans le cadre du développement et de la vérification formelle d'un
compilateur pour langage fonctionnel, nous avons fait l'expérience de
l'influence de la preuve de préservation sémantique sur la conception des
langages intermédiaires et de leurs sémantiques formelles.

Il s'agit d'un compilateur pour le fragment purement fonctionnel de ML, non
typé, vérifié formellement dans l'assistant de preuves Coq.  Dans l'esprit
des compilateurs CompCert, ce compilateur est réaliste et optimisant. En plus
d'une grande expressivité du langage source (fonctions récursives, type
concret et filtrage) et de l'implantation d'optimisations (décurryfication,
CPS, compilation optimisée des appels en position terminale), nous proposons
une interaction avec un gestionnaire de mémoire automatique à glaneur de
cellules.

Plus concrètement, nous avons développé une chaîne de compilation en amont
dont le langage cible est Cminor, le langage d'entrée du backend CompCert, ce
qui nous permet de produire du code en assembleur PowerPC.  Notre chaîne de
compilation en amont est une séquence de plusieurs transformations de
langages intermédiaires. Pour chacune de ces transformations, nous avons
montré un résultat de préservation sémantique. La composition de ces
résultats nous mène à la vérification formelle de notre compilateur.

Dans cet exposé, nous proposons une vue d'ensemble de ce compilateur et
détaillons un point important du développement : la vérification formelle de
l'interaction avec un gestionnaire de mémoire automatique au travers de deux
transformations mettant en jeu uniquement des langages purement fonctionnels
et sa concrétisation sur le modèle mémoire de Cminor.