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. 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.
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