Formal Methods
Coq for Industry
Formal verification and certified programs with the Coq proof assistant
3 days
Duration
On-site or remote
Delivery
50%
Hands-on
Overview
About this course
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.
Who is this for?
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
Outcomes
What you will learn
Install and configure Coq
Develop programs in Coq's functional language
Structure Coq projects effectively
Construct formal proofs using tactics
Extract certified programs from proofs
Syllabus
Program outline
Introduction
- –Coq presentation, applications, and ecosystem
- –Installation and environment setup
Functional Language
- –Calculus of constructions and definitions
- –Implicit arguments, sections, modules, notations
- –Standard library exploration and program evaluation
Proof Language
- –Property definitions and basic/advanced tactics
- –Ltac language and Curry-Howard isomorphism
- –Specification and proof of programs
Case Studies
- –Mini-language implementation
- –Access control policy verification
Practicalities
Before you enroll
Prerequisites
- –Strong algorithmics knowledge
- –Functional programming experience
- –Mathematical foundation
Format
- On-site or remote
- 3–10 participants
- 50% hands-on exercises
- Schedule: 9:30 - 17:30
Funding
- Qualiopi certified
- OPCO funding eligible
- Sessions on demand within 2 months
- Accessibility accommodations available
Instructors
Your trainers
Julien Blond
R&D engineer, doctorate holder, expert in formal methods, Coq verification, and cybersecurity certification.
Enroll