Assistants de preuves

 

Les assistants de preuve sont particulièrement utiles dans la vérification de composants matériels ou logiciels, et ce pour des propriétés indécidables. Afin de pallier le manque d'automaticité de la vérification, ces outils sont interactifs et accompagnés de langages permettant de programmer des stratégies de démonstration, voire même de disposer de procédures automatiques sur des fragments décidables de la théorie considérée.

L'assistant de preuve Coq est intéressant à plus d'un titre :

  • il est basé sur un langage très expressif, le Calcul des Constructions Inductives contenant la logique d'ordre supérieur intuitionniste, et permettant d'exprimer les programmes et leur spécification, ainsi que l'extraction de programmes à partir de la preuve de réalisabilité de spécifications;
  • les réductions associées à ce λ-calcul facilitent les preuves par réflexion;
  • les preuves sont représentées par des λ-termes, la validité des énoncés obtenus en utilisant les tactiques est assurée par le vérificateur de types;
  • les outils de developpement de preuves n'ont pas à être validés (critère de De Bruijn)

Les activités sur cette direction de recherche s'articulent autour des points suivants :

  • Formalisation de la théorie des calculs locaux : preuves d'algorithmes distribués, preuves de propriétés de classes d'algorithmes (simulation, résultats d'impossibilité) - Travail en collaboration avec le projet VISIDIA;
  • Etude des relations entre la logique de Coq et le langage mathématique: opérateur de choix d'Hilbert, fonctions partielles;
  • Modélisation et vérification de propriétés de sécurité de systèmes embarqués, et notamment de microprocesseurs spécialisés tels que les cartes à puces.

Les activités autour de ce sous-thème comportent donc des aspects pratiques, notamment dans la programmation de méthodes de preuve, et plus fondamentaux, concernant la puissance d'expression de divers formalismes logiques.