@@ -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
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.
