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:
- The theory of separation logic for reasoning about mutable data structures
- The application of the theory in automatic reasoning tools
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:
- A first component consisting of lectures on the main aspects of separation logic theory for sequential, concurrent and object oriented languages, as well as hands-on experience of automatic reasoning tools.
- A second component consisting of presentations by the students of a research paper to gain an in-depth knowledge of one particular aspect of the research.
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
- Introduction to separation logic
- Concurrent separation logic
- Abstract predicate families for object orientation
- Hands-on experience with automatic tools
- Each student will present a research paper in a seminar and discuss it with the class. Here are a few suggestions for paper presentations.
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 |