Accueil

Présentation de l’équipe

L’objectif de l’équipe-projet MARELLE est d’étudier les techniques
de vérification de démonstration sur ordinateur pour assurer la
correction de logiciel. Les domaines visés sont les logiciels de calcul
scientifique (calcul formel, arithmétiques des ordinateurs). L’équipe-projet
développe des méthodes et des outils pour aider à produire des
programmes corrects à partir de descriptions précises des données, des
algorithmes ainsi qu’à partir de leurs propriétés et des preuves de ces
propriétés.

Thèmes de recherche

  • Environnements de preuves
  • Formalisation des mathématiques et théorie des types
  • Algorithmique certifiée
  • Propriétés formelles des nombres, calcul exact.

Relations internationales et industrielles

  • ANR Galapagos : Géométrie, Algorithmes, Preuves
  • ANR CompCert : certification de compilateurs
  • ANR A3Pat : collaboration entre réécriture et démonstration sur ordinateur
  • Laboratoire commun INRIA/Microsoft-research : Composants mathématiques
  • TYPES Working group: raisonnement assisté par ordinateur en théorie des types
  • Université de Nice, laboratoire A. Dieudonné : formalisation de preuves mathématiques