Logo Logiciels
Et
Mathématiques
M
E

in English

 

Méthodes formelles pour la construction de logiciels sûrs.

L'objectif du projet Lemme est d'introduire et de développer les méthodes formelles dans la construction de logiciels sûrs. Les domaines 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:

  1. Environnements de preuves
  2. Formalisation des mathématiques et théorie des types
  3. Algorithmique certifiée
  4. Sémantiques des langages de programmation

Collaborations scientifiques:

  • 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.

Collaborations industrielles:

  • 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.

 
Contact: Loic.Pottier@sophia.inria.fr ou Yves.Bertot@sophia.inria.fr .
Mise à jour: 22 octobre 2001