diff --git a/teaching/separationlogic.md b/teaching/separationlogic.md index f098819eed2d36d26152a69ed9a0601298121f05..fff5bcc589ba0c3f7814194ed35d8e6320430523 100644 --- a/teaching/separationlogic.md +++ b/teaching/separationlogic.md @@ -31,7 +31,7 @@ You will learn how to write program specifications and prove properties of progr 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 our [Infer lab 2016 page](https://psvg.doc.ic.ac.uk/teaching/InferLab.html) for details + As part of the course, Facebook with Imperial ran a lab on Infer. 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.