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 15 mars, 10h30 ------------------ Stéphane Lescuyer ------------------ =============================================================== Vérification formelle et utilisation d'un solveur SMT dans Coq =============================================================== Les solveurs SMT (Satisfiability Modulo Theories) sont très prisés dans le domaine de la preuve automatique de programmes pour leur capacité à combiner efficacement des procédures de décision pour différents fragments logiques (propositionnel, arithmétique, égalité,...). Dans le domaine de la preuve interactive, et dans Coq en particulier, de nombreuses tactiques ont été implantées pour raisonner sur ces fragments, mais leur combinaison reste une tâche manuelle et fastidieuse. Je décrirai ici une implantation formelle du coeur du solveur SMT Alt-Ergo (http://alt-ergo.lri.fr) dans Coq : cette formalisation comprend un solveur SAT couplé à un algorithme de clôture par congruence modulo arithmétique linéaire. Je montrerai comment elle peut être utilisée via le mécanisme de réflexion afin d'obtenir une tactique Coq qui combine raisonnements propositionnel, arithmétique et sur l'égalité.