LEMME : Logiciels et mathématiques (projet)

En savoir plus sur le projet : Site du projet Rapport d'activité La médiathèque Rapports de recherche et thèses Thème : Sym Systèmes symboliques Unité de recherche de Sophia Antipolis

LEMME a été arrêté le 31/12/2004

Présentation du projet

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

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

Responsable scientifique

Loic POTTIER
+33 4 92 38 78 19
Loic.Pottier@inria.fr
Secrétariat : +33 4 92 38 76 00