To: seminaire@pauillac.inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 10/11/06 - Paris - FR

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

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                        Vendredi 10 novembre, 10h30

                              ---------------
                              Sylvain Conchon
                              ---------------

                                    LRI

  ========================================================================
  Ergo, un petit démonstrateur automatique dédié à la preuve de programmes
  ========================================================================

Ergo est un démonstrateur automatique de théorèmes dédié à la
vérification de propriétés de programmes. Les formules logiques
envoyées à Ergo sont écrites dans une logique du 1er ordre polymorphe
multi-sortée. L'architecture d'Ergo est basée sur deux procédures de
décision: CC(X), un algorithme de fermeture par congruence
paramétrable par une théorie equationelle X (actuellement X est
instancié par la théorie vide et l'arithmétique linéaire) et
l'algorithme de Fourier-Motzkin pour traiter les inéquations de
l'arithmétique linéaire. La partie propositionnelle des formules est
gérée par un SAT-solver qui interagit avec un mécanisme
d'instanciation pour traiter les quantificateurs. Le code d'Ergo est
très court (seulement 3000 lignes d'Ocaml) ce qui en fait un bon
candidat pour réaliser la preuve en Coq d'un démonstrateur
automatique. Ergo est disponible à: http://ergo.lri.fr