Détail d'une fiche   Version PDF

LEMME (SR0246WR)

Logiciels et mathématiques

LEMME →  MARELLE (SR0179HR)


Statut: Terminée

Responsable : Loïc Pottier

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

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

Domaine : Systèmes symboliques
Thème : Structures algébriques et géométriques, algorithmes

Période : 01/01/1992 -> 31/12/2004
Dates d'évaluation :

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 :

Numéro RNSR : 199221442W
N° de structure Inria: SR0246WR

Présentation

L'objectif du projet Lemme est d'introduire et de développer les méthodes formelles dans la construction de logiciels sûrs. Les domaine visés sont les logiciels de calcul scientifique (calcul formel, arithmétiques des ordinateurs), et les logiciels de cartes à puces. Le projet développe donc des méthodes et des outils pour aider à produire des programmes corrects à partir de descriptions mathématiques des données, des algorithmes, des langages de programation, ainsi qu'à partir de leurs propriétés et des preuves de ces propriétés. Notre outil de travail privilégié est le système Coq (équipe Démon, Université Paris-Sud, et projet Logical, INRIA Rocquencourt).


Axes de recherche

  • environnements de preuves
  • formalisation des mathématiques et théorie des types
  • algorithmique certifiée
  • sémantiques des langages de programmation


Relations industrielles et internationales

  • TYPES Working Group: raisonnement assité par ordinateur fondé sur la théorie des types.
  • Actions de recherche coopératives: AOC (Arithmétique des ordinateurs certifiée) , S-Java (Combination of formal tools for verifying security properties of Java programs).
  • Projet Mowgli (projet européen LTR): mathématiques formelles sur le Web (Universités de Bologne, de Berlin, de Nijmgen et Eindhoven, DFKI Saarbrücken, Max Planck Institute, et Trusted Logic)
  • Université de Nice, laboratoire A.Dieudonné: formalisation des shémas en géométrie algébrique.
  • Université de Minho: théorie des types.
  • Université de la République (Uruguay) et de Université de Cordoba (Argentine): méthodes formelles pour les cartes à puce.
  • Contrat européen Verificard: modélisation et vérification de la plate-forme et des programmes Javacard (GemPlus, Bull, Universités de Nimegue, Munich, Hagen, Sics).
  • Dassault: traitement de la récursion bien fondée en Coq.