Sites Inria

English version

Equipe de recherche STAMP

• Sûreté du logiciel et Preuves Mathématiques Formalisées

Présentation de l'équipe

L'équipe-project STAMP s'intéresse à la vérification formelle d'algorithmes et de résultats mathématiques à l'aide d'outils de preuve interactive comme Coq ou Easycrypt.  Les domaines d'applications privilégiés concernent la cryptographie et la robotique formalisée.  Les contributions logicielles les plus notables portent sur le système de preuve Coq, le système de preuve EasyCrypt, et la bibliothèque de mathématiques formalisées Mathematical Components.

Axes de recherche

Théorie des types; Théorie de la preuve; Vérification formelle; Cryptographie; Robotique; Génération et transformation automatique de preuves formelles; Génération et transformation automatique de programmes sûrs

Suivez Inria