To: seminaire-gallium-moscova@inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 07/12/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 7 decembre, 11h15 --------------------- Jean-Baptiste Tristan --------------------- INRIA ================================================== Formal verification of translation validation (a 15-minute talk, plus ample time for discussion) ================================================== Translation validation consists in transforming a program and then checking that the semantics has been preserved. This approach can be used in mechanically verified compilation provided that the validator has been proved correct. I will present two such validators that have been designed to verify program transformations that optimize the instruction paralellism.