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 - 2024" : 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

Mots-clés de "B - Autres sciences et domaines d'application - 2024" : 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/2028
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/Rocq.  Un domaine d'applications privilégié concerne la robotique formalisée.  Les contributions logicielles les plus notables portent sur le système de preuve Coq/Rocq, la bibliothèque de mathématiques formalisées Mathematical Components et l'outil de métaprogrammation Elpi.


Axes de recherche

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


Relations industrielles et internationales