To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 06/07/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 6 juillet, 10h30

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

                                   INRIA

                 ==========================================
                 Certification par Validation de Traduction
                 ==========================================

La validation de traduction consiste à transformer un programme et à le
valider a posteriori afin de détecter d'éventuelles modifications de sa
sémantique. Cette approche peut être utilisée en compilation certifiée à
condition de prouver formellement que la validation est correcte. Je
présenterai deux telles validations destinées à la certification
d'optimisations tirant parti du parallélisme d'instructions des processeurs.