Collège de France

Sciences du logiciel - Xavier Leroy

Technology FR ↓ 73 episodes

Écrire un petit programme informatique est facile. Concevoir et réaliser un logiciel complet qui soit fiable, pérenne et résistant aux attaques reste extraordinairement difficile. C'est le but des sciences du logiciel que de concevoir et développer les principes, les formalismes mathématiques, les techniques empiriques et les outils informatiques nécessaires pour concevoir, programmer et vérifier des logiciels fiables et sécurisés. L'enseignement de la chaire Sciences du logiciel vise à explorer cette problématique et à présenter la recherche contemporaine dans ce domaine. Le cours privilégie...

Author

Collège de France

Episodes

03 - Logiques de programmes : quand la machine raisonne sur ses logiciels 18.03.2021 1:25:53

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Dans le troisième cours, nous avons étudié les structures de données et la vérification de programmes qui les manipulent. Les tableaux sont la plus ancienne des structures de données. Une extension simple de la logique de Hoare avec une règle pour l'affectation à...

02 - Logiques de programmes : quand la machine raisonne sur ses logiciels 11.03.2021 1:22:36

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Le deuxième cours a été consacré à l'étude approfondie des « logiques de Hoare », c'est-à-dire des logiques de programmes qui suivent l'approche introduite par C. A. R. Hoare en 1969. Nous avons défini une telle logique de programmes pour le langage IMP, un petit...

01 - Logiques de programmes : quand la machine raisonne sur ses logiciels 04.03.2021 1:14:46

Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Résumé Comment s'assurer qu'un logiciel fait ce qu'il est censé faire ? Les méthodes classiques de vérification et de validation du logiciel, reposant sur le test, les revues et les analyses, ne suffisent pas toujours. La vérification déductive permet d'aller plus...

08 - Sémantiques mécanisées : quand la machine raisonne sur ses langages 13.02.2020 1:11:02

Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages

07 - Sémantiques mécanisées : quand la machine raisonne sur ses langages 06.02.2020 1:25:41

Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages

06 - Sémantiques mécanisées : quand la machine raisonne sur ses langages 30.01.2020 1:16:42

Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages

05 - Sémantiques mécanisées : quand la machine raisonne sur ses langages 16.01.2020 1:20:18

Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages

04 - Sémantiques mécanisées : quand la machine raisonne sur ses langages 09.01.2020 1:57:58

Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages

03 - Sémantiques mécanisées : quand la machine raisonne sur ses langages 19.12.2019 1:22:36

Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages

02 - Sémantiques mécanisées : quand la machine raisonne sur ses langages 12.12.2019 1:20:43

Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages

01 - Sémantiques mécanisées : quand la machine raisonne sur ses langages 28.11.2019 1:49:12

Xavier Leroy Collège de France Science du logiciel Année 2019-2020 Sémantiques mécanisées : quand la machine raisonne sur ses langages

11 - Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui 30.01.2019 1:01:39