@@ -26,9 +26,9 @@ The course comprises two hours a week for seven weeks. It is be accompanied by c
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.
You will learn about Smallfoot, a semi-automatic verification tool based on symbolic execution, and Infer, 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.
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/).
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
* The last week will provide an introduction to concurrent separation logics. With Brookes, O'Hearn won the Godel prize for this work in 2016.
