Episodes
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 cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes. La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint...
Published 04/15/21
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 cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes. La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint...
Published 04/08/21
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 cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes. La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint...
Published 04/08/21
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 cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes. La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint...
Published 04/01/21
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 cinquième cours, nous avons étudié quatre extensions des logiques de séparation des précédents cours qui permettent ou facilitent la spécification et la vérification d'une plus large classe de programmes. La première extension est l'opérateur d'implication séparante, familièrement appelé « baguette magique » en raison de sa forme, qui est l'adjoint...
Published 04/01/21
Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Les processeurs multicœurs sont un exemple d'architecture parallèle à mémoire partagée, où plusieurs unités de calcul travaillent simultanément sur une mémoire commune. La programmation de ces architectures est difficile : il faut maîtriser les interférences possibles entre les actions des processus, et éviter les courses critiques (race conditions) entre...
Published 03/25/21
Xavier Leroy Collège de France Science du logiciel Année 2020-2021 Logiques de programmes : quand la machine raisonne sur ses logiciels Les processeurs multicœurs sont un exemple d'architecture parallèle à mémoire partagée, où plusieurs unités de calcul travaillent simultanément sur une mémoire commune. La programmation de ces architectures est difficile : il faut maîtriser les interférences possibles entre les actions des processus, et éviter les courses critiques (race conditions) entre...
Published 03/25/21
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 à un élément d'un tableau permet de spécifier et de vérifier de nombreux programmes utilisant des...
Published 03/18/21
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 à un élément d'un tableau permet de spécifier et de vérifier de nombreux programmes utilisant des...
Published 03/18/21
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 langage impératif à contrôle structuré que nous avions déjà étudié dans le cours 2019-2020 «...
Published 03/11/21
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 langage impératif à contrôle structuré que nous avions déjà étudié dans le cours 2019-2020 «...
Published 03/11/21
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 loin en établissant des propriétés vraies de toutes les exécutions possibles d'un programme,...
Published 03/04/21
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
Published 02/26/20
Published 02/26/20
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
Published 02/26/20
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
Published 02/26/20
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
Published 02/13/20
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
Published 02/13/20
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
Published 02/13/20
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
Published 02/12/20
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
Published 02/12/20
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
Published 02/12/20
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
Published 02/06/20