Coq for Industry
Formal verification and certified programs with the Coq proof assistant
3 days
Durée
On-site or remote
Modalités
50%
Pratique
Aperçu
À propos de ce cours
Description
An industrial-focused, three-day formal methods course introducing participants to the Coq proof assistant. Covers language fundamentals, proof development, and practical applications for modeling and verifying programs.
À qui s'adresse cette formation ?
You need to formalize computing systems in Coq to enhance system reliability and safety for critical software.
Software developers with formal methods interestVerification engineersSafety-critical systems engineers
Objectifs
Ce que vous allez apprendre
01
Install and configure Coq
02
Develop programs in Coq's functional language
03
Structure Coq projects effectively
04
Construct formal proofs using tactics
05
Extract certified programs from proofs
Programme
Plan de la formation
01
Introduction
- —Coq presentation, applications, and ecosystem
- —Installation and environment setup
02
Functional Language
- —Calculus of constructions and definitions
- —Implicit arguments, sections, modules, notations
- —Standard library exploration and program evaluation
03
Proof Language
- —Property definitions and basic/advanced tactics
- —Ltac language and Curry-Howard isomorphism
- —Specification and proof of programs
04
Case Studies
- —Mini-language implementation
- —Access control policy verification
Infos pratiques
Avant de vous inscrire
Prérequis
- —Strong algorithmics knowledge
- —Functional programming experience
- —Mathematical foundation
Format
- On-site or remote
- 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
R&D engineer, doctorate holder, expert in formal methods, Coq verification, and cybersecurity certification.
S'inscrire