Material for the course
'Logical Investigations on Separation Logics'
ESSLLI 2015, Barcelona
ESSLLI 2015
This site contains
course notes and reference materials for the
ESSLLI course 'Logical Investigations on Separation Logics' to be given on August 10-14 2015, Barcelona,
and
prepared by
Stéphane Demri
and Morgan Deters (in memoriam).
Course Description
Separation logic is a well-known formalism to
extend Hoare logic to verify programs with pointers. In this course,
we propose to investigate the logical side of separation logics by presenting
material about models, decidability, computational complexity, expressive power and decision procedures
including those based on SMT solvers. Motivations for formal verification are also provided.
Furthermore, we emphasize the similarities between separation logic and, modal or temporal logics.
These are standard themes for studying logics in computer science and
we deliberately focus on the logical side of separation logic.
Prerequisites
This is the material that we assume you have already seen and will simply be mentioned in the lectures.
- Basics of logic including first-order logic and temporal logic
- Basics of complexity theory, decidability
Course material
A draft version of the lecture notes is available
here.
Slides will be available on a daily basis.
The course comprise ten 40-min lectures, delivered 2 per day,
with a 5 min break in between.
- Day 1: First Steps in Separation Logics --
Slides.
- Day 2: Propositional Separation Logics --
Slides.
- Day 3: Expressive Power: First-Order Separation Logics --
Slides.
- Day 4: Relationships with Other Logics --
Slides.
- Day 5: Decision Procedures --
Slides.
The documents that can be downloaded below are preprints that have been usually obtained from the authors' pages.
In order to make precise references to these papers, the versions available by the publishers should be preferred.
Surveys
Useful readings -- Day 1
Useful readings -- Day 2
Useful readings -- Day 3
Useful readings -- Day 4
Useful readings -- Day 5