Accueil Accueil

JDEV 2015 - Grand Amphi-session du vendredi
Coq, un assistant de preuve. (6533) - Vendredi 03 juillet 2015 09:15 - 10:15

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

Informatique

Toutes les vidéos de l'évenement JDEV 2015 - Grand Amphi-session du vendredi (5 videos)

00:26:13.90

2015-07-03

08:30 - 09:15 : Devlog

01:20:07.88

2015-07-03

09:15 - 10:15 : Coq, un assistant de preuve.

00:19:00.86

2015-07-03

10:15 - 10:30 : Retour d'expérience de l'utilisation de coq chez un industriel

00:50:34.57

2015-07-03

11:00 - 11:45 : JavaScript: de la standardisation à la formalisation

00:08:36.96

2015-07-03

12:00 - 12:30 : Conclusion, présentation CEPAge et remerciements JDEV15

Contact Webcast

La cellule webcast du CCIN2P3 vous propose de diffuser en direct et/ou en différé sur internet vos manifestations, colloques, conférences. Attention, ce service est réservé au domaine public dans le domaine de la Recherche Scientifique.


Cellule Webcast
Centre de Calcul IN2P3/CNRS
21 Avenue Pierre de Coubertin
CS70202
69627 VILLEURBANNE Cedex

Tél. :
+33(0) 4.78.93.08.80

Fax. :
+33(0) 4.72.69.41.70



Email :

Voir les mentions légales du site