Equipe de recherche LEMME

Logiciels et mathématiques

  • Responsable : Loic Pottier
  • Centre(s) de recherche : Sophia Antipolis - Méditerranée
  • Domaine : Systèmes symboliques
  • Thème : Structures algébriques et géométriques, algorithmes

Présentation de l'équipe

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.

Siège et centres de recherche Inria

Accès direct

Social