Vous pouvez vous abonner à nos annonces de séminaires
                     http://gallium.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 20 juin, 10h30

                                -----------
                                Paolo Herms
                                -----------

                              CEA-LIST / INRIA

                   ======================================
                       Certification d'une chaîne de
                   vérification déductive de programmes
                   ======================================

Je présente la formalisation en Coq d'un générateur de conditions de
vérification sur un langage de programmation sans alias inspiré par l'outil
Why. Ce langage sera la cible d'une compilation certifiée d'un sous-ensemble
du langage C avec annotations logiques.