Newsgroups: fr.announce.seminaires
Distribution: fr
To: fr-sem@frmug.org
From: Hugo.Herbelin@inria.COUPER-CECI.fr
Organization: INRIA-Rocquencourt
Subject: SEM - INRIA : Coq - 14/03/2000 - Paris - FR

           http://pauillac.inria.fr/bin/calendar/Seminaires


                             S E M I N A I R E

   ____              ____    .                   
  /   _   _        /    ___   __  /_  _   /     /| /|  _   __ __ _       _ 
 /   / \ / \  _   /    /   / /_  /   __| /  _  / |/ | / \ /_ /  / \ | / __|
|___ |_/ |_/     |___ /   / __/ |_  |_/ |_    /     | |_/__/ |_ |_/ |/ |_/
          /                                                                 
         /                                                                  
                          I N R I A - Rocquencourt, 
                       Salle de conference du Bat 11

                        Mardi 14 mars, 10h30h-17h30

                   -------------------------------------
                   Journée spéciale (rappel et horaires)
                   -------------------------------------


         ==========================================================
         Comparaison de formalisations en Coq, HOL, Isabelle et PVS
         ==========================================================


  10h30 Accueil - Café

  11h Tristan Crolard (LACL - Université de Créteil)
     Formalisation et vérification du problème du "passage à niveau"
     dans Coq et PVS.

  14h Laurent Théry (INRIA Sophia)
     Une comparaison de Coq, Hol, Pvs : une preuve élémentaire de
     l'algorithme à clé public RSA

  15h Jean-Paul Bodeveix (IRIT - Université de Toulouse)
     Formalisation de la méthode B en Coq et PVS
     Travail commun avec Mamoun Filali et César Muñoz

  16h30 Pierre Casteran (LABRI - Université de Bordeaux)
     Preuves sur les systèmes de transitions en Isabelle/HOL et
     partiellement en Coq (travail commun avec Davy Rouillard)

  Résumés disponibles à "http://coq.inria.fr/seminaires/comparaison".
La page restera en place après la journée avec le matériel fourni par
les orateurs. Pour se rendre à l'INRIA, consulter la page
"http://www.inria.fr/Allera/Somm-aller-fra.html".