Logiques de programmes : quand la machine raisonne sur ses logiciels

Documents et médias

Télécharger le programme

pdf (286 Ko)

Programme

Cours

09:30 - 11:00

Comment raisonner sur un logiciel ? La naissance des logiques de programmes

Xavier Leroy

04 Mar 2021

Logiques de programmes : quand la machine raisonne sur ses logiciels

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Variables et boucles : la logique de Hoare

Xavier Leroy

11 Mar 2021

Logiques de programmes : quand la machine raisonne sur ses logiciels

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Les logiques de programmes à l'épreuve du réel : tours et détours avec Frama-C/WP

Loïc Correnson

11 Mar 2021

Logiques de programmes : quand la machine raisonne sur ses logiciels

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

VeriFast: Semi-Automated Modular Verification of Concurrent C and Java Programs Using Separation Logic

Bart Jacobs

25 Mar 2021

Logiques de programmes : quand la machine raisonne sur ses logiciels

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Quelques extensions de la logique de séparation

Xavier Leroy

01 Avr 2021

Logiques de programmes : quand la machine raisonne sur ses logiciels

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Raisonner à propos du temps en logique de séparation

François Pottier

01 Avr 2021

Logiques de programmes : quand la machine raisonne sur ses logiciels

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Logiques pour la mémoire partagée faiblement cohérente

Xavier Leroy

08 Avr 2021

Logiques de programmes : quand la machine raisonne sur ses logiciels

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Protocoles personnalisés en logique de séparation : ressources fantômes et invariants dans la logique Iris

Jacques-Henri Jourdan

08 Avr 2021

Logiques de programmes : quand la machine raisonne sur ses logiciels

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Logiques pour les langages fonctionnels et l'ordre supérieur

Xavier Leroy

15 Avr 2021

Logiques de programmes : quand la machine raisonne sur ses logiciels

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

Gillian: a Multi-language Platform for Compositional Symbolic Analysis

Philippa Gardner

15 Avr 2021

Logiques de programmes : quand la machine raisonne sur ses logiciels

Amphithéâtre Guillaume Budé, Site Marcelin Berthelot

15 Avr 2021

11:15 - 12:15

Voir aussi

Cours en relation avec le séminaire : Logiques de programmes : quand la machine raisonne sur ses logiciels

Xavier Leroy, chaire Sciences du logiciel

Logiques de programmes : quand la machine raisonne sur ses logiciels

Documents et médias

Programme

Comment raisonner sur un logiciel ? La naissance des logiques de programmes

Variables et boucles : la logique de Hoare

Les logiques de programmes à l'épreuve du réel : tours et détours avec Frama-C/WP

Pointeurs et structures de données : la logique de séparation

Preuve auto-active de programmes en SPARK

Parallélisme à mémoire partagée : la logique de séparation concurrente

VeriFast: Semi-Automated Modular Verification of Concurrent C and Java Programs Using Separation Logic

Quelques extensions de la logique de séparation

Raisonner à propos du temps en logique de séparation

Logiques pour la mémoire partagée faiblement cohérente

Protocoles personnalisés en logique de séparation : ressources fantômes et invariants dans la logique Iris

Logiques pour les langages fonctionnels et l'ordre supérieur

Gillian: a Multi-language Platform for Compositional Symbolic Analysis

Voir aussi