This 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.
#### Description of the Course
...
...
@@ -19,17 +20,17 @@ As well as Facebook, Infer is used by Instagram, kiuwan, oculus, Spotify, UBER,
#### Course Outline
The course comprises two hours a week for seven weeks.
It will be accompanied by comprehensive course notes, which bring together a variety of ideas from the most influential research papers.
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.
*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.
* 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.
Facebook will run a lab on Infer on 14th November.
The last week will provide an introduction to concurrent separation logics.
With Brookes, O'Hearn won the Godel prize for this work in 2016.
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. For details on the 2016 infer lab please follow the [link](http://fbinfer.com/).
* The last week will provide an introduction to concurrent separation logics. With Brookes, O'Hearn won the Godel prize for this work in 2016.
