Equipe de recherche MARELLE

Mathématiques, Raisonnement et Logiciel

Présentation de l'équipe

L'objectif de l'équipe-projet MARELLE est d'étudier l'utilisation de 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.

Axes 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 industrielles et internationales

  • 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

Mots-clés : Formalisation d'algorithmes mathématiques Démonstration sur ordinateur

Equipes de recherche du même thème :

Siège et centres de recherche Inria

Accès direct

Social