11 Mar 2021 → 15 Apr 2021 Seminar Program logic : when the machine reasons about its software 11 Mar 2021 → 15 Apr 2021 Share Facebook X (ex-Twitter) Linkedin Copy url
from Thursday 11 March to Thursday 15 April 2021 See also: Related LectureXavier Leroy Documents and media Download program pdf (286 KB) Program Lecture 09:30 - 11:00 How to reason about software The birth of program logic Xavier Leroy 04 Mar 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 04 Mar 2021 09:30 - 11:00 Lecture 09:30 - 11:00 Variables and loops : Hoare logic Xavier Leroy 11 Mar 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 11 Mar 2021 09:30 - 11:00 Seminar 11:15 - 12:15 Program logic put to the test : twists and turns with Frama-C/WP Loïc Correnson 11 Mar 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 11 Mar 2021 11:15 - 12:15 Lecture 09:30 - 11:00 Pointers and data structures : separation logic Xavier Leroy 18 Mar 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 18 Mar 2021 09:30 - 11:00 Seminar 11:15 - 12:15 Auto-active proof of programs in SPARK Yannick Moy 18 Mar 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 18 Mar 2021 11:15 - 12:15 Lecture 09:30 - 11:00 Parallelism with shared memory : the logic of concurrent separation Xavier Leroy 25 Mar 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 25 Mar 2021 09:30 - 11:00 Seminar 11:15 - 12:15 VeriFast: Semi-Automated Modular Verification of Concurrent C and Java Programs Using Separation Logic Bart Jacobs 25 Mar 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 25 Mar 2021 11:15 - 12:15 Lecture 09:30 - 11:00 Some extensions of the separation logic Xavier Leroy 01 Apr 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 01 Apr 2021 09:30 - 11:00 Seminar 11:15 - 12:15 Reasoning about time in separation logic François Pottier 01 Apr 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 01 Apr 2021 11:15 - 12:15 Lecture 09:30 - 11:00 Weakly coherent shared memory logic Xavier Leroy 08 Apr 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 08 Apr 2021 09:30 - 11:00 Seminar 11:15 - 12:15 Custom protocols in separation logic : ghost resources and invariants in Iris logic Jacques-Henri Jourdan 08 Apr 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 08 Apr 2021 11:15 - 12:15 Lecture 09:30 - 11:00 Logics for functional and higher-order languages Xavier Leroy 15 Apr 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 15 Apr 2021 09:30 - 11:00 Seminar 11:15 - 12:15 Gillian: a Multi-language Platform for Compositional Symbolic Analysis Philippa Gardner 15 Apr 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 15 Apr 2021 11:15 - 12:15 See also Lecture related to the seminar: Program logic : when the machine reasons about its software Xavier Leroy, chair Software Science
Lecture 09:30 - 11:00 How to reason about software The birth of program logic Xavier Leroy 04 Mar 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 04 Mar 2021 09:30 - 11:00
Lecture 09:30 - 11:00 Variables and loops : Hoare logic Xavier Leroy 11 Mar 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 11 Mar 2021 09:30 - 11:00
Seminar 11:15 - 12:15 Program logic put to the test : twists and turns with Frama-C/WP Loïc Correnson 11 Mar 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 11 Mar 2021 11:15 - 12:15
Lecture 09:30 - 11:00 Pointers and data structures : separation logic Xavier Leroy 18 Mar 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 18 Mar 2021 09:30 - 11:00
Seminar 11:15 - 12:15 Auto-active proof of programs in SPARK Yannick Moy 18 Mar 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 18 Mar 2021 11:15 - 12:15
Lecture 09:30 - 11:00 Parallelism with shared memory : the logic of concurrent separation Xavier Leroy 25 Mar 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 25 Mar 2021 09:30 - 11:00
Seminar 11:15 - 12:15 VeriFast: Semi-Automated Modular Verification of Concurrent C and Java Programs Using Separation Logic Bart Jacobs 25 Mar 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 25 Mar 2021 11:15 - 12:15
Lecture 09:30 - 11:00 Some extensions of the separation logic Xavier Leroy 01 Apr 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 01 Apr 2021 09:30 - 11:00
Seminar 11:15 - 12:15 Reasoning about time in separation logic François Pottier 01 Apr 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 01 Apr 2021 11:15 - 12:15
Lecture 09:30 - 11:00 Weakly coherent shared memory logic Xavier Leroy 08 Apr 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 08 Apr 2021 09:30 - 11:00
Seminar 11:15 - 12:15 Custom protocols in separation logic : ghost resources and invariants in Iris logic Jacques-Henri Jourdan 08 Apr 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 08 Apr 2021 11:15 - 12:15
Lecture 09:30 - 11:00 Logics for functional and higher-order languages Xavier Leroy 15 Apr 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 15 Apr 2021 09:30 - 11:00
Seminar 11:15 - 12:15 Gillian: a Multi-language Platform for Compositional Symbolic Analysis Philippa Gardner 15 Apr 2021 Program logic : when the machine reasons about its software Amphithéâtre Guillaume Budé, Site Marcelin Berthelot 15 Apr 2021 11:15 - 12:15
