Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Démonstration automatique (24h, 3 ECTS)

Responsables : Évelyne Contejean et Ralf Treinen

Intervenants prévus pour 2014-2015

  • Ralf Treinen (4 cours = 12h)
  • Mohamed Iguernelala (4 cours = 12 heures)

Évaluation

  • Projet SMT (Mohamed Iguernelala) à rendre pour le 19/03/2015
  • Examen final (Ralf Treinen) le 12/03/2015, de 9h45 à 11h45. Tous les documents papier sont autorisés.

Note = (P + E)/2

Objectifs

Le but de ce cours est de fournir aux étudiants les bases nécessaires afin de pouvoir comprendre le fonctionnement de la plupart des outils de démonstration automatique développés en particulier dans le monde académique (voir la page TPTP), et éventuellement de coder eux-mêmes de tels outils.

Naturellement, ce cours est nécessaire pour les étudiants qui poursuivraient ensuite des travaux de recherche dans le domaine de la vérification, de la démonstration automatique ou de la récriture, mais aussi dans des domaines connexes comme la sécurité des systèmes informatiques, les systèmes embarqués, les preuves assistées et plus généralement l'utilisation des systèmes formels.

Plan du cours pour 2014-2015

Ralf Treinen (4 cours) : Résolution de contraintes symboliques et théories du premier ordre

Dans cette partie du cours nous nous intéressons à des contraintes, c'est-à-dire à des formules de la logique du premier ordre interprétées dans une structure fixée. Une formule avec n variables, interprétée dans une structure fixe, dénote un ensemble de n-uplets de valeurs qui est simplement son ensemble de solutions. La possibilité de combiner des formules par des opérateurs booléens ou des quantificateurs, ensemble avec un algorithme pour décider la satisfaisabilité des formules, nous donne un moyen effectif pour calculer avec des ensembles de n-uplets de valeurs. Des tels mécanismes sont à la base des formalismes computationnels qui manipulent des ensembles de n-uplets de valeurs, comme par exemple la programmation (logique) par contraintes, la réécriture contrainte, ou la vérification de systèmes infinis.
La présentation est organisée autour des méthodes générales. Les méthodes présentées sont illustrées par des systèmes de contraintes utilisées dans les mécanismes mentionnées, typiquement sur des nombres naturels ou des valeurs symboliques (arbres).

  • Contraintes de base: simplification, satisfaisabilité, implication
  • Élimination de quantificateurs
  • Méthodes basées sur des classes d'automates
  • Méthodes pour les preuves de non-décidabilité de théories

Mohamed Iguernelala (4 cours) : Solveurs Modulo Théories (SMT)

  • SAT solveurs modernes (back-jumping, learning), MiniSat ;
  • interaction entre SAT et une procédure de décision pour une théorie T : DPLL(T) ;
  • exemples de théories qui ont une procédure de décision :
    • tableaux ;
    • arithmétique linéaire ;
    • égalité
  • combinaison de procédures de décision ;
  • traitement des quantificateurs par le mécanisme des déclancheurs (triggers) ;
  • exemples de solveurs SMT : Alt-Ergo, CVS4, Simplify, Yices, Z3

Planning:

  • 11 décembre Ralf Treinen
  • 18 décembre Ralf Treinen
  • 8 janvier Ralf Treinen
  • 15 janvier Ralf Treinen
  • 22 janvier Mohamed Iguernelala
  • 29 janvier Mohamed Iguernelala
  • 5 février Mohamed Iguernelala
  • 12 février Mohamed Iguernelala
  • 12 mars : examen final (voir les modalités d'évaluation plus haut)

Pré-requis

Notions de logique du premier ordre, savoir ce qu'est une règle d'inférence.

Langues du cours :

  • Français par défaut / French by default
  • Les langues autorisées pour l'examen sont le français et l'anglais.

Supports de cours :

Le polycopié et les transparents de la partie de Ralf Treinen se trouvent sur http://www.pps.univ-paris-diderot.fr/~treinen/teaching/mpri2.5/.
Le polycopié contient plus de matériel que ce que l'on peut effectivement traiter en 4 session de cours.

Cours liés :

  • Recommandé :
    • 2-36-1 preuve de programmes
    • 2-7-1 fondements des systèmes de preuves
    • 2-7-2 : assistants de preuves
  • Pour la culture

Bibliographie

L'essentiel du cours se trouve dans

  • A. Robinson and A. Voronkov eds, Handbook of Automated Reasoning, vols 1 & 2, North Holland, 2001.
  • Nachum Dershowitz and Jean-Pierre Jouannaud, Rewrite systems, Handbook of Theoretical Computer Science (vol. B): Formal Models and Semantics, MIT Press, Cambridge, MA, 1991

Sur des parties importantes du cours:

Équipe pédagogique

Sylvain Conchon MC UPSud LRI
Évelyne Contejean CR CNRS LRI
Pierre Courtieu MC CNAM CEDRIC
Mohamed Iguernelala UPsud OcamlPro/LRI
Ralf Treinen PU P7 PPS
Xavier Urbain MC ENSIIE CEDRIC
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA