Preuve mécanisée

Mots-clés

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

Description

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 :

  1. la conception et le développement de systèmes de preuves, notamment :
    • la conception du formalisme du λΠ-calcul modulo théories, mis en pratique à travers du vérificateur de preuves Dedukti et de l'assistant de preuve LambdaPi
    • la participation au développement de l'assistant de preuve Isabelle
    • la participation au développement de la Méthode B et Event-B
  2. l'interopérabilité entre systèmes de preuves, par la conception, l'utilisation et la transformation de certificats de preuve
  3. le développement de bibliothèques et formalisations pour des thématiques variées :
    • pour les données
    • pour les mathématiques
    • pour la preuve de programmes

Logiciels

Deducteam

Logiciels autour de Dedukti et LambdaPi

FormalData

Formalisation autour des données en Coq

Isabelle/C

Plateforme pour le test et la preuve de programmes C en Isabelle

Logipedia

Bibliothèque universelle de preuves

SMTCoq et Sniper

Outils de vérification de preuves automatiques et d'automatisation pour Coq

Publications

Liste complète sur HAL : https://hal.science/LMF-PM

Séminaires, groupes de travail

  • Séminaire Deducteam régulier le jeudi après-midi

Projets

Projet ANR ICSPA

Assistants de preuve basés sur la théorie des ensembles interopérables et sûrs

Projet bilatéral franco-japonais (partenariat Hubert Curien)

Members

Permanent

PhD Students

Luc Chabassier

Xavier Denis

Houda MOUHCINE

Melanie Taprogge

PostDoc

Alidra Abdelghani

Anthony Bordg

Matteo Manighetti