Introduction

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