Détail d'une fiche   Version PDF

STAMP (SR0883FR)

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

MARELLE (SR0179HR) →  STAMP


Statut: Décision signée

Responsable : Yves Bertot

Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2023" : A2.1.11. Langages de preuve , A2.4.3. Preuves , A4.5. Méthodes formelles pour la sécurité , A7.2. Logique , A7.2.3. Assistants de preuve , A7.2.4. Formalisation mécanisée des mathématiques , A8.3. Géométrie, Topologie , A8.4. Calcul formel, calcul algébrique , A8.10. Arithmétique des ordinateurs

Mots-clés de "B - Autres sciences et domaines d'application - 2023" : B6.1. Industrie du logiciel , B9.5.1. Informatique , B9.5.2. Mathématiques

Domaine : Algorithmique, programmation, logiciels et architectures
Thème : Preuves et vérification

Période : 01/11/2019 -> 31/12/2024
Dates d'évaluation :

Etablissement(s) de rattachement : <sans>
Laboratoire(s) partenaire(s) : <sans UMR>

CRI : Centre Inria d'Université Côte d'Azur
Localisation : Centre Inria d'Université Côte d'Azur
Code structure Inria : 041162-0

Numéro RNSR : 201923413W
N° de structure Inria: SR0883FR

Présentation

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


Relations industrielles et internationales