Méthodes formelles
Coq pour l'industrie
Vérification formelle et programmes certifiés avec l'assistant de preuve Coq
3 jours
Durée
Sur site ou à distance
Modalités
50%
Pratique
Aperçu
À 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.
Développeurs logiciels intéressés par les méthodes formellesIngénieurs en vérificationIngénieurs systèmes critiques
Objectifs
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
Programme
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
Infos pratiques
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
Instructeurs
Vos formateurs
Julien Blond
Ingénieur R&D, docteur, expert en méthodes formelles, vérification Coq et certification cybersécurité.
S'inscrire