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](http://www.imperial.ac.uk/computing), [Imperial College London](http://www.imperial.ac.uk).
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](http://www.imperial.ac.uk/computing), [Imperial College London](http://www.imperial.ac.uk).
The course is led by [Philippa Gardner](/people/gardner.html), with support
from [Jose Fragoso](https://www.doc.ic.ac.uk/~jfaustin/) and [Julian Sutherland](https://psvg.doc.ic.ac.uk/people/sutherland.html).
#### Description of the Course
#### Description of the Course
In the late 1960s, Tony Hoare developed Hoare logic, a formal system with a set of rules for reasoning rigorously about the correctness of imperative programs that alter the variable state. However, Hoare logic is not good at reasoning about imperative programs that alter the heap state, since the reasoning does not scale.
In the late 1960s, Tony Hoare developed Hoare logic, a formal system with a set of rules for reasoning rigorously about the correctness of imperative programs that alter the variable state. However, Hoare logic is not good at reasoning about imperative programs that alter the heap state, since the reasoning does not scale.
In 2001, building on Hoare's work and early ideas from Burstall, O'Hearn and Reynolds introduced separation logic, in which the reasoning does scale. This course will provide a whirl-wind tour of separation logic, its verification tools and cutting-edge research on reasoning about concurrent programs.
In 2001, building on Hoare's work and early ideas from Burstall, O'Hearn and Reynolds introduced separation logic, in which the reasoning does scale.
This course will provide a whirl-wind tour of separation logic, its verification tools and cutting-edge research on reasoning about concurrent programs.
Separation logic was introduced to reason about shared mutable data structures represented in the heap: in particular, to catch memory overruns and null-pointer dereferencing.
Separation logic was introduced to reason about shared mutable data structures represented in the heap: in particular, to catch memory overruns and null-pointer dereferencing.
It has been used to reason about C, Java and JavaScript programs, and algorithms for shared-memory concurrency.
It has been used to reason about C, Java and JavaScript programs, and algorithms for shared-memory concurrency.
There are many academic verification tools, such as [Smallfoot](http://www0.cs.ucl.ac.uk/staff/p.ohearn/smallfoot/), [Verifast](https://people.cs.kuleuven.be/~bart.jacobs/verifast/) and Abductor, and the industrial tool [Infer](http://fbinfer.com/), developed by a team led by Peter O'Hearn at Facebook.
There are many academic verification tools, such as [Smallfoot](http://www0.cs.ucl.ac.uk/staff/p.ohearn/smallfoot/), [Verifast](https://people.cs.kuleuven.be/~bart.jacobs/verifast/) and Abductor, and the industrial tool [Infer](http://fbinfer.com/), developed by a team led by Peter O'Hearn at Facebook.
...
@@ -35,28 +35,77 @@ This work constitutes a breakthrough, in that it is now possible prove propertie
...
@@ -35,28 +35,77 @@ This work constitutes a breakthrough, in that it is now possible prove propertie
* The last week will provide an introduction to concurrent separation logics. With Brookes, O'Hearn won the Godel prize for this work in 2016.
* 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 2017 autumn term
#### General Information for 2018 autumn term
Time: Tuesdays 4pm-6pm, 2nd--9th week
Time: Tuesdays 2pm-4pm, 2nd through 9th week, Room 140.
Coursework Published: Monday 6th of November
Coursework Published Tue 30th Oct, 9 AM / deadline Fri 9th Nov, 4 PM.
Submitted: Thursday 16th of November by 16:00
Exam: The exam will take place on Tuesday, December 11th, at 11:40, room TBC. It will last for 70 minutes.
You will be given three questions, out of which you need to answer two of your choice.
Feedback: Tuesday 21st of November
Recommended Reading: Mike Gordon has some [excellent notes on Hoare logic](http://www.cl.cam.ac.uk/archive/mjcg/HL/),
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.
Exam: TBC 11th week
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](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/localreasoning.pdf),
CSL 2001, and John Reynolds' [undergraduate course notes on separation logic](http://www.cs.cmu.edu/~jcr/copenhagen08.pdf)
and survey paper [Separation Logic: A Logic for Shared Mutable Data Structures](https://www.cs.cmu.edu/~jcr/seplogic.pdf),
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](http://www.imperial.ac.uk/admin-services/library/)).
Papers describing tool techniques include: [Symbolic Execution with Separation
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](https://piazza.com) site and below.
If you have further suggestions on what reading material might be of interest, please let us know.
Recommended Reading: Mike Gordon has some [excellent notes on Hoare logic](http://www.cl.cam.ac.uk/archive/mjcg/HL/), which briefly touches on separation logic in the last chapter.
Public lecture by Tony Hoare entitled ["Could computers understand their own programs?"](http://www.cambridgephilosophicalsociety.org/) on Nov. 19 at 6pm
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.
Alan Turing describes [his work on soundness, completeness, Gödel's theorem, Turing machines etc.](http://www.youtube.com/watch?v=S23yie-779k&t=28m26s)
Excellent introductions to separation logic include: O'Hearn, Reynolds and Yang's paper on [Local Reasoning about Programs that Alter Data Structures](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/localreasoning.pdf), CSL 2001, and John Reynolds' [undergraduate course notes on separation logic](http://www.cs.cmu.edu/~jcr/copenhagen08.pdf) and survey paper [Separation Logic: A Logic for Shared Mutable Data Structures](https://www.cs.cmu.edu/~jcr/seplogic.pdf), 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](http://www.imperial.ac.uk/admin-services/library/)).
Papers describing tool techniques include: [Symbolic Execution with Separation Logic](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.64.2006&rep=rep1&type=pdf), Berdine, Calcagno, O'Hearn, APLAS'05; [A Local Shape Analysis based on Separation Logic](http://www.eecs.qmul.ac.uk/~ddino/papers/localshape.pdf), Distefano, O'Hearn, Yang, TACAS 2006; and [Compositional Shape Analysis by Means of Bi-abduction](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/jacm-abduction-webversion.pdf), Calcagno, Distefano, O'Hearn, Yang, JACM 2011.
and his seminal 1967 paper [Assigning meanings to programs](http://www.cs.berkeley.edu/~necula/Papers/FloydMeaning.pdf)
Wikipedia article on [Hoare](http://en.wikipedia.org/wiki/Tony_Hoare)
and his seminal 1969 paper [An axiomatic basis for computer programming](http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf)
[Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems](http://www.cs.cmu.edu/~emc/papers/Conference%20Papers/79_impossible_hoareaxiom.pdf) by Edmund M. Clarke Jr.
Wikipedia article on [Material Implication](http://en.wikipedia.org/wiki/Material_conditional)
the [Paradoxes of Material Implication](http://legacy.earlham.edu/~peters/courses/log/mat-imp.htm)
and some [classic fallacies](http://www.math.toronto.edu/mathnet/falseProofs/fallacies.html)
Collection of [Software Bugs and Software Glitches](http://www5.in.tum.de/~huckle/bugse.html)
The VCC verifier can be downloaded from http://vcc.codeplex.com or tried at http://www.rise4fun.com/vcc
Peter Homeier's [Sunrise system](http://www.cis.upenn.edu/~hol/sunrise/)
[Design by Contract](http://www.eecs.ucf.edu/~leavens/JML/jmldbc.pdf)(a paper by Gary T. Leavens and Yoonsik Cheon)
The initial paper on concurrent separation logic is [Resources, Concurrency and Local Reasoning](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/concurrency.pdf), O'Hearn, TCS, 2007, and is worth a read.
The survey paper [Steps in Modular Specifications of Concurrent Modules](https://www.doc.ic.ac.uk/~pg/papers/mfps15.pdf), 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](https://piazza.com) site.
If you have further suggestions on what reading material might be of interest, please let us know.
