Reasoning About Programs in Higher-Order Concurrent Separation Logic
Talk at PLMW'21
Abstract.
Higher-order concurrent separation logic has been very successful in verifying correctness of intricate programs and reasoning about programming languages. In this talk we will present some basic ideas of program verification, separation logic, and how to use higher-order concurrent separation logic to reason about programs and programming languages. In particular, we will present and discuss the Iris program logic which is a general framework for defining separation logics and using them to reason about programs and programming languages.
Download & Links
- Slides: [.pdf]
- https://iris-project.org
List of Iris related talks at POPL'21 and co-located events
| Talk | Event | Date & Time (CET) |
|---|---|---|
| Toward Complete Stack Safety for Capability Machines Authors: Aïina Linn Georges, Armaël Guéneau, Alix Trieu, Lars Birkedal | PriSC'21 | Jan 17 2021 – 20:12 |
| Contextual Refinement of the Michael-Scott Queue (Proof Pearl) Authors: Simon Friis Vindum, Lars Birkedal | CPP'21 | Jan 18 2021 – 17:00 |
| Reasoning About Monotonicity in Separation Logic Authors: Amin Timany, Lars Birkedal | CPP'21 | Jan 18 2021 – 17:15 |
| [T4] Iris -- A Modular Foundation for Higher-Order Concurrent Separation Logic Authors: Tej Chajed, Ralf Jung, Joseph Tassarotti | Tutorials | Jan 18 2021 – 18:00 |
| Machine-Checked Semantic Session Typing Authors: Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, Jesper Bengtson | CPP'21 | Jan 18 2021 – 18:30 |
| Fully Abstract from Static to Gradual Authors: Koen Jacobs, Amin Timany, Dominique Devriese | POPL'21 | Jan 20 2021 – 16:00 |
| Efficient and Provable Local Capability Revocation using Uninitialized Capabilities Authors: Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Sander Huyghebaert, Dominique Devriese, Lars Birkedal | POPL'21 | Jan 21 2021 – 16:00 |
| Mechanized Logical Relations for Termination-Insensitive Noninterference Authors: Simon Oddershede Gregersen, Johan Bay, Amin Timany, Lars Birkedal | POPL'21 | Jan 21 2021 – 16:10 |
| A Separation Logic for Effect Handlers Authors: Paulo Emílio de Vilhena, François Pottier | POPL'21 | Jan 22 2021 – 16:15 |
| Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic Authors: Léon Gondelman, Simon Oddershede Gregersen, Abel Nieto, Amin Timany, Lars Birkedal | POPL'21 | Jan 22 2021 – 16:25 |