The Separation Logic course is a 4th year MEng and MSc course on local reasoning about programs that manipulate the heap at the Department of Computing, Imperial College London. The course is led by Philippa Gardner, with support from Jose Fragoso, Daiva Naudžiūnienė, Azalea Raad and Julian Sutherland.
Description of the Course
The course comprises two hours a week for seven weeks. It is be accompanied by comprehensive course notes, which bring together a variety of ideas from the most influential research papers.
The first four weeks will provide a basic introduction to separation logic for reasoning about mutable data structures, using linked lists and binary trees as the primary examples. You will learn how to write program specifications and prove properties of programs, both informally using sketch proofs and formally using rigorous proofs.
The next two weeks will describe tools, demonstrating that reasoning about real-world programs using separation logic is feasible. You will learn about Smallfoot, a semi-automatic verification tool based on symbolic execution, and Infer, an automatic tool based on bi-abduction. This work constitutes a breakthrough, in that it is now possible prove properties about millions of lines of code, thus making the reasoning viable for industry.
As part of the course, Facebook with Imperial ran a lab on Infer. See our Infer lab 2016 page for details
The last week will provide an introduction to concurrent separation logics. With Brookes, O’Hearn won the Godel prize for this work in 2016.
General Information for 2016 autumn term
Time: Mondays 2pm-4pm, 2nd–9th week
Coursework Published: Monday 7th of November
Submitted: Wednesday 16th of November
Feedback: Monday 21st of November
Exam: 11th week
Recommended Reading: Mike Gordon has some excellent notes on Hoare logic, which briefly touches on separation logic in the last chapter. Two good books on Hoare logic are: Logic in Computer Science: Modelling and Reasoning about Systems, Michael Huth and Mark Ryan, CUP, 2004; and The Formal Semantics of Programming Languages: an Introduction, Glynn Winskel, MIT Press, 1993.
Most of the work on separation logic is in research papers. Excellent introductions to separation logic include: O’Hearn, Reynolds and Yang’s paper on Local Reasoning about Programs that Alter Data Structures, CSL 2001, and John Reynolds’ undergraduate course notes on separation logic and survey paper Separation Logic: A Logic for Shared Mutable Data Structures, LICS 2002, both found on Reynolds’ homepage. Andrew Appel has published a book on Program Logics for Certified Compilers, CUP 2014 (a copy is available in the library).
Papers describing tool techniques include: Symbolic Execution with Separation Logic, Berdine, Calcagno, O’Hearn, APLAS’05; A Local Shape Analysis based on Separation Logic, Distefano, O’Hearn, Yang, TACAS 2006; and Compositional Shape Analysis by Means of Bi-abduction, Calcagno, Distefano, O’Hearn, Yang, JACM 2011.
The initial paper on concurrent separation logic is Resources, Concurrency and Local Reasoning, O’Hearn, TCS, 2007, and is worth a read. The survey paper Steps in Modular Specifications of Concurrent Modules, da Rocha Pinto, Dinsdale-Young, Gardner, MFPS 2015, describes some modern developments in concurrent separation logics. There are many additional interesting links given on the Piazza site. If you have further suggestions on what reading material might be of interest, please let us know.