To: seminaire@pauillac.inria.fr
From: Hugo.Herbelin@inria.fr
Subject: SEM - INRIA : LogiCal - 09/03/01 - Paris - FR

      Vous pouvez maintenant vous abonner à nos annonces de séminaires
             http://pauillac.inria.fr/seminaires/subscribe.html


                             S E M I N A I R E
                                         . ___ 
                           /   _   _      /   _   /
                          /   / \ / \  / /   __| /
                         |___ |_/ |_/ / |__ |_/ |_
       ___      .                  /    
      /    ___   __  /_  _   /   _/        /| /|  _   __ __ _       _ 
     /    /   / /_  /   __| /             / |/ | / \ /_ /  / \ | / __|
    |___ /   / __/ |_  |_/ |_            /     | |_/__/ |_ |_/ |/ |_/
                                                
                          I N R I A - Rocquencourt
                       Salle de conference du Bat 11

                           Vendredi 9 mars, 10h30

                                -----------
                                Pablo Argon
                                -----------

                           Cadence Berkeley Labs

   =====================================================================
   Formalisation et extraction en Coq du prouveur de l'outil Cadence-SMV
   =====================================================================


   L'outil de vérification Cadence-SMV, conçu et développé par Kenneth
   McMillan, permet de vérifier des propriétés temporelles de systèmes de
   grande taille, voire infinis, grâce à la combinaison d'une
   vérificateur sur modèle symbolique et d'un prouveur spécialisé.  Son
   intérêt pratique a déjà été mis en évidence sur de nombreux exemples
   industriels : preuve de l'algorithme de Tomasulo, preuve de plusieurs
   "cache coherence protocols", etc.  Cependant, dans l'implémentation
   actuelle du système plusieurs erreurs ont été relevées,
   particulièrement dans le prouveur spécialisé
   
   Pour cette raison, depuis environ un an, nous avons formalisé une
   version simplifiée du prouveur spécialisé de SMV (toutes les règles
   n'ont pas été traitées) dans l'assistant à la preuve Coq, afin de
   pouvoir à la fois prouver la correction des règles de décomposition,
   et extraire le code implémentant la décomposition, c'est-à-dire le
   prouveur spécialisé, grâce aux techniques de certification et
   d'extraction de programmes uniques de Coq.
   
   Dans cet exposé nous donnerons un aperçu de ce travail en présentant
   les principales étapes suivies pour arriver au <<prototype>> du
   nouveau système SMV basé sur un prouveur spécialisé extrait depuis la
   preuve formelle faite en Coq et interfacé avec un vérificateur sur
   modèle développé spécialement.