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, with support from Jose Fragoso, Daiva Naudziuniene, Azalea Raad and Julian Sutherland.
The course is led by [Philippa Gardner](/people/gardner.html), with support
from [Jose Fragoso](https://www.doc.ic.ac.uk/~jfaustin/), [Daiva Naudžiūnienė](https://www.doc.ic.ac.uk/~dn911/),
[Azalea Raad](http://www.soundandcomplete.org/) and [Julian Sutherland](https://psvg.doc.ic.ac.uk/people/sutherland.html).
#### Description of the Course
#### Description of the Course
...
@@ -28,7 +30,8 @@ You will learn how to write program specifications and prove properties of progr
...
@@ -28,7 +30,8 @@ You will learn how to write program specifications and prove properties of progr
* The next two weeks will describe tools, demonstrating that reasoning about real-world programs using separation logic is feasible.
* 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](http://fbinfer.com/), an automatic tool based on bi-abduction.
You will learn about Smallfoot, a semi-automatic verification tool based on symbolic execution, and [Infer](http://fbinfer.com/), 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.
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.
Facebook with Imperial ran a lab on Infer on 14th November. See the [Infer lab 2016 page](https://psvg.doc.ic.ac.uk/teaching/InferLab.html) for details
Facebook with Imperial ran a lab on Infer on 14th November. See our [Infer lab 2016 page](https://psvg.doc.ic.ac.uk/teaching/InferLab.html) 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.
* The last week will provide an introduction to concurrent separation logics. With Brookes, O'Hearn won the Godel prize for this work in 2016.
