Date de début:
09:00
Date de fin:
10:00
Lieu:
Bordeaux INP - ENSEIRB-MATMECA
Ville:
Bordeaux
Producteur:
-

Durée:
1:20:08
Type:
video/mp4
Poids:
515.94 Mo
Format:
mp4
Résolution:
1280x720
Codec:
-

Coq, un assistant de preuve.


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

Dernières vidéos