To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 28/04/08 - 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

                           Lundi 28 avril, 10h30

                           ---------------------
                           Jean-Baptiste Tristan
                           ---------------------

                                   INRIA

            ===================================================
            Vérification formelle de validateurs de traduction:
                  une étude de cas sur le lazy code motion
            ===================================================

Le lazy code motion est une transformation de programme qui
permet à la fois une élimination globale des sous-expressions
communes, l'élimination des redondances partielles et la
factorisation des invariants de boucles. Cette optimisation
repose sur plusieurs analyses globales de flot de données et sa
preuve de préservation sémantique paraît difficile. Dans cet
exposé, je montrerai comment, en utilisant la technique de
validation de traduction, nous avons pu développer une passe de
lazy code motion qui préserve la sémantique. Enfin, ceci nous
amènera à considérer un validateur plus général pour la famille
des optimisations dont le but est l'élimination des calculs
redondants.