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 - 26/05/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 conférence du Bât 11

                           Vendredi 26 mai, 10h30

                               -------------
                               Laurent Théry
                               -------------

                           INRIA Sophia-Antipolis

         ==========================================================
         Une comparaison de Coq, Hol,Pvs: une preuve élémentaire de
                       l'algorithme à clé public RSA
         ==========================================================

Dans cet exposé, nous présentons une preuve élémentaire de
l'algorithme RSA qui a été réalisée dans 3 démonstrateurs différents:
Coq, HOL et PVS. Après une rapide présentation de la preuve,
nous montrerons comment les spécificités des différents 
démonstrateurs ont influé sur la preuve.