Coq, un assistant de preuve

Résumé

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?

 
jdev2015/p.v1.txt · Dernière modification: 2015/05/29 17:27 par elodie.bourrec@irap.omp.eu
 
Recent changes RSS feed Powered by PHP Powered by Pxxo Driven by DokuWiki