Détail d'une fiche   Version PDF

MARELLE (SR0179HR)

Mathématiques, Raisonnement et Logiciel

LEMME (SR0246WR) →  MARELLE →  STAMP (SR0883FR)


Statut: Terminée

Responsable : Yves Bertot

Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2023" : Aucun mot-clé.

Mots-clés de "B - Autres sciences et domaines d'application - 2023" : Aucun mot-clé.

Domaine : Algorithmique, programmation, logiciels et architectures
Thème : Preuves et vérification

Période : 01/11/2006 -> 31/10/2019
Dates d'évaluation : 22/03/2011 , 17/03/2015 , 20/03/2019

Etablissement(s) de rattachement : <sans>
Laboratoire(s) partenaire(s) : <sans UMR>

CRI : Centre Inria d'Université Côte d'Azur
Localisation : Centre Inria d'Université Côte d'Azur
Code structure Inria : 041020-1

Numéro RNSR : 200618405J
N° de structure Inria: SR0179HR

Présentation

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.

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