Preuve mécanisée

Mots-clés

  • preuve automatique
  • preuve interactive
  • interopérabilité des systèmes de preuve
  • cadre logiques
  • vérification croisée
  • Dedukti
  • Logipedia

Cette équipe regroupe les concepteurs des outils de preuve mécanisée, des systèmes eux-mêmes jusqu'aux bibliothèques, assurant ainsi un continuum. Elle s'organise en trois axes : la conception et le développement de systèmes de preuves, l'interopérabilité entre systèmes de preuves, et le développement de bibliothèques et formalisations pour des thématiques données.

Axe 1 : Conception et développement de systèmes de preuve

L'équipe est le principal concepteur et développeur des systèmes de preuve suivants.

Le formalisme du lambda-pi calcul modulo théorie

Membres: Bruno Barras, Frédéric Blanqui, Valentin Blot, Gilles Dowek, Gabriel Hondet, Amélie Ledein

Le lambda-pi calcul modulo théorie est un cadre logique développé par l'équipe depuis une dizaine d'années qui généralise divers cadres logiques précédents (calcul des prédicats, Isabelle, lambda-Prolog, pure type systems, théorie des types de Martin-Löf, lambdapi-calcul) et permet l'encodage de nombreuses logiques et systèmes de preuve actuels (HOL Light, Isabelle/HOL, Matita, Coq, Agda). Il est implémenté dans le système Dedukti. Cela soulève de nombreux problèmes théoriques et pratiques:

  • Comment encoder dans le lambda-pi calcul modulo théorie, de manière correcte et complète, les fonctionalités des systèmes de preuve actuels (proof irrelevance, predicate subtyping, inductive and co-inductive definitions, cubical type theory, etc.) tout en préservant certaines propriétés du lambda-pi calcul (terminaison, confluence, préservation du typage)?
  • Comment comparer et traduire de l'un dans l'autre dans le lambda-pi calcul modulo théorie deux systèmes de preuve différents?
  • Peut-on équiper Dedukti d'une interface et d'un mécanisme de preuve interactif? Cela permettrait de vérifier directement dans Dedukti la combinaison de preuves réalisées dans différents prouveurs sans avoir à les traduire (e.g. si on a prouvé A=>B dans X et A dans Y, a-t-on effectivement B? si oui, dans quel système?). Les fonctionalités particulières à Dedukti (réécriture, buts d'unification) permettent également de définir des objets mathématiques complexes qu'il est difficile, voire impossible, à définir dans les systèmes actuels (e.g. les infini-catégories).

Logiciels: https://github.com/Deducteam



Il participe également au développement des systèmes suivants.

Isabelle

Membres : Idir Ait-Sadoune, Nicolas Meric, Safouan Taha, Burkhart Wolff

Au dela des developpements substantielles variés de libraries pour l' Archive of Formal Proofs (Isabelle/AFP), qui couvre des domaines fondamentales (HOL-CSP, UTP, Clean, TESL-Semantics ... ) ou applicatives (Network-Models, Security Policies, UML-Model-Transformations, OS-Kernels ...), il y a une tradition de developpements des "tools-as-components-on-top" du noyau d'Isabelle. Coté noyau, le groupe a été impliqué dans l'amelioration de sa parallelisation (Projet ANR-ParalITP 2011-2016). Coté outils, les systèmes

ont été developpés.

Il y a une groupe de discussion plus ou moins régulier concernant tout les aspects d'Isabelle, le Isabelle-Club.

Méthodes B/Event-B

Membres : Idir Ait-Sadoune, Guillaume Verdier (Post-doc)

L'objectif de cet axe est d'étudier l'extension de la méthode Event-B pour prendre en charge les développements de systèmes complexes nécessitant la modélisation d’objets mathématiques et le support des preuves associées. Plus précisément, permettre aux modèles Event-B d'importer et d'utiliser des théories de domaine. Concernant la vérification des théories définies et importées, il est important de proposer un système de preuve qui étend les prouveurs actuels de la méthode Event-B pour prendre en charge cette extension et intégrer au processus de preuve les définitions importées à partir des théories référencées.

Axe 2 : Interactions entre systèmes de preuves, bibliothèques universelles

La multiplicité des systèmes de preuve permet aujourd'hui de vérifier formellement et de manière la plus automatisée possible des énoncés complexes et variés. Cependant, cela s'accompagne d'une duplication des efforts extrêmement prononcée : valider une preuve dans un système donné demande de formaliser tous les pré-requis dans ce système, même s'ils existent par ailleurs. L'objectif de cet axe est de travailler à l'interopérabilité entre systèmes de preuve, et de proposer une bibliothèque de preuves formalisées que l'on peut importer dans la plupart des systèmes.

Certificats de preuve

Membres : Frédéric Blanqui, Valentin Blot, Boris Djalal, Gilles Dowek, Yacine El Haddad, Quentin Garchery, Chantal Keller, Claude Marché, Andrei Paskevich, Mihaela Sighireanu, Pierre Vial

L'objectif est d'explorer les preuves comme protocole de communication entre systèmes de preuves, afin d'échanger des résultats et de valider ceux-ci au sein d'un même système. Cette approche est mise en pratique dans les aspects suivants :

  • Interaction sûre entre prouveurs interactifs et prouveurs automatiques : l'objectif est de faire bénéficier chacun des deux systèmes des avantages de l'autre à travers l'échange de certificats : d'une part, via des encodages, les prouveurs interactifs pourront bénéficier de davantage d'automatisation ; d'autre part, les prouveurs automatiques pourront valider leurs résultats à l'aide d'un outil certifié. Cela est mis en pratique notamment dans l'outil SMTCoq, dont le but est de faire interagir l'assistant de preuve Coq avec des prouveurs automatiques du premier ordre (de type SMT : Satisfiabilité Modulo Théories). Une autre application est l'utilisation de prouveurs SMT en logique de séparation, pour la sécurité, ou encore pour la preuve de programmes.
  • Conception de certificats de preuves : l'objectif est de concevoir et générer des certificats de preuves pour divers outils. Dans ce cadre, l'outil ekstrakto a pour but de générer des certificats de preuves à partir de sorties de prouveurs automatiques du premier ordre. Une autre application est la génération de certificats pour les outils de preuve de programmes, et notamment les calculs d'obligation de preuves effectués dans Why3.

Logiciels : SMTCoq, Sniper, ekstrakto

Groupe de travail DigiCosme UPSCaLe

Logipedia

Membres : Bruno Barras, Frédéric Blanqui, Valentin Blot, Gilles Dowek, Chantal Keller, Burkhart Wolff

Logipédia est une bibliothèque de preuves universelle, contenant une base de théorèmes issues de l'assistant de preuve Matita et qu'il est possible d'importer dans les assistants de preuve Coq, Matita, Lean et PVS, et dans le format de preuves d'ordre supérieur Open Theory.

Bibliothèque : Logipedia

Axe 3 : Formalisations et développement de bibliothèques

Pour les données

Membres : Véronique Benzaken, Évelyne Contejean, Chantal Keller, Rébecca Zucchini

Cet axe couvre la formalisation de résultats fondamentaux en science des données, le développement d'outils certifiés pour la manipulation de données, et de bibliothèques pour la formalisation des langages centrés données. Les aspects étudiés sont :

  • la formalisation de langages centrés données et de compilateurs pour ces langages
  • la formalisation de mécanismes afférents à la manipulation des données, comme la sécurité ou la provenance des données.

Projet : DataCert

Groupe de travail DigiCosme Transform

Pour les mathématiques

Membres : Sylvie Boldo

La résolution des équations aux dérivées partielles (EDP) est au cœur de nombreux programmes de simulation dans l'industrie et la méthode des éléments finis (MEF) est un outil très populaire pour leur résolution numérique. Il s'agit de poser les fondements qui nous permettront de prouver la correction d'une bibliothèque implantant la MEF en C++, telle que FELiScE (Finite Elements for Life Sciences and Engineering). Sa vérification formelle augmentera la confiance dans tous les codes qui l'utilisent. Ce projet est interdisciplinaire avec l'analyse numérique.

Ces preuves reposent entre autres sur la théorie de la mesure, l'intégrale de Lebesgue, les distributions et les espaces de Sobolev. Nous souhaitons formaliser et prouver en Coq les bases mathématiques jusqu'à la construction de l'espace fonctionnel L 2 ainsi que les propriétés afférentes, en particulier la complétude pour la norme associée au produit scalaire.

Pour la preuve de programmes

Membres : Jean-Christophe Filliâtre, Jacques-Henri Jourdan, Andrei Paskevich, Mihaela Sighireanu, Burkhart Wolff

La preuve de programmes nécessite des bibliothèques de plusieurs natures : d'une part, des bibliothèques pour spécifier et prouver (séquence, ensembles, dictionnaires, etc.) ; d'autre part, des bibliothèques de programmes déjà prouvés servant de briques de bases (des structures de données, notamment, mais pas uniquement). Ces deux sortes de bibliothèques ne sont pas disjointes. Le code fantôme, par exemple, utilise des bibliothèques de programmes dans une activité liée exclusivement à la spécification et à la preuve. Le degré d'automatisation des preuves que l'on peut espérer dans la preuve de programmes dépend fortement de la façon dont ces bibliothèques ont été conçues.

Bibliothèques : Iris, vocal, stdlib Why3

On peut finalement aussi mentionner:

  • Isabelle/C Plateforme pour Test et Preuve des Programmes C

Bibliothèques de lemmes pour la preuve d'algorithmes sur les structures de données dynamiques (en C ou Ada). Ce travail a été effectuée pour l'outil Verifast pour la vérification de programmes C avec la logique de séparation. Il peut être étendu à d'autres structures de données et d'autres outils.

Members

Permanent

PhD Students

Luc Chabassier

Xavier Denis

Yoan Geran

Nicolas Meric

Houda Mouhcine

Vaishnav Rishikesh

Andrew Samokish

Rébecca Zucchini

PostDoc

Claude Stolze