To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 21/09/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
                         Amphi Turing du bâtiment 1

                        Vendredi 21 septembre, 10h30

                                ------------
                                Xavier Leroy
                                ------------

                          INRIA Paris-Rocquencourt

    ===================================================================
                Raisonner sur les programmes qui divergent:
    deux approches suivies dans la vérification du compilateur Compcert
    ===================================================================


                       "L'éternité, c'est long, surtout vers la fin."
                       (Woody Allen)

Compcert est un compilateur C vérifié, c'est-à-dire accompagné d'une
preuve Coq que la sémantique du programme source est préservée tout au
long de la chaîne de compilation.  Initialement, cette preuve ne
s'appliquait qu'aux programmes source qui terminent: les sémantiques
naturelles utilisées pour les différents langages de Compcert ne
permettaient pas de raisonner sur des programmes qui divergent. Dans
cet exposé, je décrirai les modifications majeures apportées à la
preuve de Compcert pour lever cette restriction. Après une
présentation des deux techniques sémantiques utilisées pour rendre
compte de la divergence (sémantiques à transitions et sémantiques
naturelles coinductives), je montrerai comment une preuve de
préservation sémantique pour une passe de compilation, initialement
menée avec des sémantiques naturelles et limitée au cas "terminant",
peut être convertie de manière semi-systématique pour utiliser l'une
de ces deux techniques et s'étendre aux programmes divergents.