From 842b315b7eef68e5679198ce71fa61fd12c80f02 Mon Sep 17 00:00:00 2001 From: Teresa Carbajo-Garcia <t.carbajo-garcia@imperial.ac.uk> Date: Wed, 30 Nov 2016 13:11:51 +0000 Subject: [PATCH] Update separationlogic.md --- teaching/separationlogic.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/teaching/separationlogic.md b/teaching/separationlogic.md index 21d810b..d8c4ae4 100644 --- a/teaching/separationlogic.md +++ b/teaching/separationlogic.md @@ -7,7 +7,9 @@ menu_order: 5 --- 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 @@ -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. 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. -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. -- GitLab