Coq pour l'industrie
Vérification formelle et programmes certifiés avec l'assistant de preuve Coq
À propos de ce cours
Description
Une formation de trois jours en méthodes formelles, orientée industrie, qui initie les participants à l'assistant de preuve Coq. Elle couvre les fondamentaux du langage, le développement de preuves et des applications pratiques pour modéliser et vérifier des programmes.
À qui s'adresse cette formation ?
Vous devez formaliser des systèmes informatiques en Coq afin de renforcer la fiabilité et la sûreté de logiciels critiques.
Ce que vous allez apprendre
Installer et configurer Coq
Développer des programmes dans le langage fonctionnel de Coq
Structurer efficacement des projets Coq
Construire des preuves formelles à l'aide de tactiques
Extraire des programmes certifiés à partir de preuves
Plan de la formation
Introduction
- –Présentation de Coq, applications et écosystème
- –Installation et configuration de l'environnement
Langage fonctionnel
- –Calcul des constructions et définitions
- –Arguments implicites, sections, modules, notations
- –Exploration de la bibliothèque standard et évaluation de programmes
Langage de preuve
- –Définition de propriétés et tactiques de base/avancées
- –Langage Ltac et isomorphisme de Curry-Howard
- –Spécification et preuve de programmes
Études de cas
- –Implémentation d'un mini-langage
- –Vérification d'une politique de contrôle d'accès
Avant de vous inscrire
Prérequis
- –Solides connaissances en algorithmique
- –Expérience en programmation fonctionnelle
- –Bases mathématiques
Format
- Sur site ou à distance
- 3–10 participants
- 50% exercices pratiques
- Horaires : 9h30 - 17h30
Financement
- Certifié Qualiopi
- Éligible OPCO
- Sessions sur demande sous 2 mois
- Accessibilité PMR et adaptations possibles
Vos formateurs
Julien Blond
Ingénieur R&D, docteur, expert en méthodes formelles, vérification Coq et certification cybersécurité.