Coq est un “assistant de preuve”, c'est à dire un logiciel permettant le développement interactif de démonstrations. Ces démonstrations sont vérifiées sur machine avant d'être acceptées comme preuves formelles. Outre ses applications en mathématiques, où il a permis de de mener à bien des démonstrations avec un niveau de confiance jamais encore atteint, Coq trouve ses applications en certification du logiciel.
Nous présenterons quelques exemples d'applications où cette technologie a permis d'obtenir un niveau de confiance maximum dans des composants logiciels critiques. Puis nous aborderons les points suivants: - Quel niveau scientifique/technique est nécessaire pour l'utilisation de cet outil? - Dans quelles applications est-il rentable? - Quel degré de confiance attribuer à un logiciel prouvé avec Coq?