Separation Logic

Cristiano Calcagno, Bertrand Meyer, Fall 2011

General

News

31.10.2011 — Added a tentative schedule for paper presentations.

24.10.2011 — Added suggestions for paper presentations.

17.08.2011 — Website up and running.

Course description

252-2602-00L Separation Logic

Abstract

"Separation Logic Theory and Applications" covers two main aspects of recent developments in separation logic:

Objectives

By taking this course, students will become familiar with the fundamental concepts of separation logic and the current state of the art of research in the subject.
The course includes two components:

Content

"Separation Logic Theory and Applications" is divided into two parts: a block of lectures, and a block of presentations from the separation logic literature given by the students.

PART I: LECTURES

PART II: SEMINARS

Lectures

Organization

Stephan van Staden is the organizing assistant for the course. Please contact him if you have questions.

Schedule

Note that this is a compact course. It runs over three (non-consecutive) weeks.

Week Time Location
24-28 Oct 17:00-18:00 IFW D 42
14-18 Nov 17:00-18:00 IFW D 42
21-25 Nov 17:00-18:00 IFW D 42

Slides

Date Title Slides
Mon. 24.10 Introduction Slides Slides (with animations)
Tue. 25.10 Program Logic Slides
Wed. 26.10 Introduction to separation logic for OO Slides
Thu. 27.10 Separation logic for OO: method specification and verification (Included in the slides of Wednesday)
Fri. 28.10 Tools

Paper Presentations

This part of the course is organized in seminar-style. Every student is required to give a 20 minute presentation of a chosen research paper.

Date Presentation 1 Presentation 2
Mon. 14.11 Alejandro Garcia: Symbolic Execution with Separation Logic. J Berdine, C Calcagno and PW O'Hearn. Proceedings of APLAS'05. Maria Christakis: Smallfoot: Modular Automatic Assertion Checking with Separation Logic. J Berdine, C Calcagno and PW O'Hearn. In 4th FMCO, LNCS 4111, 2006
Tue. 15.11 Milos Novacek: A local shape analysis based on separation logic. D Distefano, P O'Hearn and H Yang. In TACAS 2006. Valentin Wuestholz: Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn and Hongseok Yang. Footprint Analysis: A Shape Analysis that Discovers Preconditions (SAS 2007)
Wed. 16.11 Tobias Hartmann: Resources, Concurrency and Local Reasoning. Peter O'Hearn. CONCUR 2004
Thu. 17.11 Uri Juhasz: Bornat et al. - Permission Accounting in Separation Logic, POPL 2005 Simon Hudon: A Fresh Look at Separation Algebras and Share Accounting, by Hobor Aquinas and Robert Dockins and Andrew W. Appel, APLAS 2009
Fri. 18.11 Simone Frau: Inferring invariants in Separation Logic for imperative list-processing algorithms. S Magill, A Nanevsky, E Clarke and P Lee, SPACE 2006
Mon. 21.11 Mischael Schill: jStar: Towards Practical Verification for Java. Dino Distefano and Matthew Parkinson. OOPSLA 2008 Malte Schwerhoff: Parkinson et al - The Relationship Between Separation Logic and implicit dynamic frames. ESOP 2011