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?

Pierre CASTERAN Pierre Castéran est maître de conférences à l'Université de Bordeaux. Il est co-auteur d'un ouvrage de référence sur le logiciel Coq et a co-organisé plusieurs écoles d'été sur ce thème en France, en Chine et au Japon