research/gillian.md

@@ -7,7 +7,7 @@ menu_order: 4
 sub_menu_order: 2
 ---
 
-Gillian is a multi-language platform for the development
+[Gillian](https://gillianplatform.github.io/) is a multi-language platform for the development
 of compositional symbolic analysis tools. Gillian currently
 supports three flavours of analysis: symbolic
 testing, full verification based on separation logic, and
@@ -55,4 +55,4 @@ and GCHQ. It was previously supported by the EPSRC programme grant
 
 [VeTSpec]: https://gow.epsrc.ukri.org/NGBOViewGrant.aspx?GrantRef=EP/R034567/1
 [EP/K008528/1]: http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/K008528/1
-[REMS]: http://www.cl.cam.ac.uk/~pes20/rems/
+[REMS]: http://www.cl.cam.ac.uk/~pes20/rems/
\ No newline at end of file

teaching/ModelsComputation.md

@@ -15,17 +15,15 @@ The course focuses on teaching students the fundamental skills involved in deali
 This course provides a whirlwind tour of some of the key concepts in theoretical computer science. 
 In particular, we will study formal descriptions (models) of computational behaviour. 
 
-#### General Information for 2019 autumn term
+#### General Information for 2021 autumn term
 
-Time: 	Wednesdays: 9am - 11am, Room 311.
-
-Thursdays: 12 - 1pm, Room 311.
+Time: 	Mondays: 11am - 12am, Room TBC and Fridays: 4pm - 6pm, Room TBC.
 
 Coursework Schedule: 
 
-Assesed coursework 1: published Weds 30th Oct, 9 AM / deadline for submission Fri 8th Nov, 4 PM.
+Assesed coursework 1: published TBC / deadline for submission TBC.
 
-Assesed coursework 2: published Wed 27th Nov, 9 AM / deadline for submission Tue 10th Dec, 4 PM. 
+Assesed coursework 2: TBC / deadline for submission TBC. 
 
 Tutorials: Tutorial exercises will be posted online (here and on CATE) before the tutorial each week, printed copies will also be available. 
 Tutorial solutions will be published online before the next week's tutorial.

teaching/separationlogic.md

 ---
-title: Separation Logic 
+title: Scalable Software Verification 
 project_id: sl
 menu: false
 parent_menu: Teaching
@@ -7,12 +7,11 @@ menu_order: 5
 sub_menu_order: 1
 ---
 
-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 Scalable Software Verification course (formerly Separation Logic)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).
 
 #### Description of the Course
 
-In the late 1960s, Tony Hoare developed Hoare logic, a formal system with a set of rules for reasoning rigorously about the correctness of imperative programs that alter the variable state. However, Hoare logic is not good at reasoning about imperative programs that alter the heap state, since the reasoning does not scale.
-In 2001, building on Hoare's work and early ideas from Burstall, O'Hearn and Reynolds introduced separation logic, in which the reasoning does scale. 
+In the late 1960s, Tony Hoare developed Hoare logic, a formal system with a set of rules for reasoning rigorously about the correctness of imperative programs that alter the variable state. However, Hoare logic is not good at reasoning about imperative programs that alter the heap state, since the reasoning does not scale. In 2001, building on Hoare's work and early ideas from Burstall, O'Hearn and Reynolds introduced separation logic, in which the reasoning does scale. 
 
 This course will provide a whirl-wind tour of separation logic, its verification tools and cutting-edge research on reasoning about concurrent programs.
 Separation logic was introduced to reason about shared mutable data structures represented in the heap: in particular, to catch memory overruns and null-pointer dereferencing. 
@@ -35,11 +34,11 @@ This work constitutes a breakthrough, in that it is now possible prove propertie
 
 * The last week will provide an introduction to concurrent separation logics. With Brookes, O'Hearn won the Godel prize for this work in 2016.
 
-#### General Information for 2019 autumn term
+#### General Information for 2021 autumn term
 
-*Time:*  Tuesdays 2pm-4pm, 2nd through 9th week, Room 130.
+*Time:*  Mondays 2pm-4pm, 2nd through 9th week, Room 145 and Thursdays 11am-1pm, 2nd through 9th week, Room 145
 
-*Coursework:* Published Tues 29th Oct, 9 AM / deadline Fri 8th Nov, 4 PM.
+*Coursework:* Published TBC / deadline TBC.
 
 *Exam:* The exam will take place December, date and time TBC. It will last for 70 minutes. 
 You will be given three questions, out of which you need to answer two of your choice.
@@ -75,18 +74,17 @@ da Rocha Pinto, Dinsdale-Young, Gardner, MFPS 2015, describes some modern develo
 There are many additional interesting links given on the [Piazza](https://piazza.com) site and below.
 If you have further suggestions on what reading material might be of interest, please let us know.
 
-Public lecture by Tony Hoare entitled ["Could computers understand their own programs?"](http://www.cambridgephilosophicalsociety.org/) on Nov. 19 at 6pm
+Public lecture by Tony Hoare entitled ["Could computers understand their own programs?"](https://www.cl.cam.ac.uk/seminars/wheeler/tony-hoare/), part of the annual Wheeler lectures series.
 
-Alan Turing describes [his work on soundness, completeness, Gödel's theorem, Turing machines etc.](http://www.youtube.com/watch?v=S23yie-779k&t=28m26s) 
+A re recording of a broadcast by Alan Turing, describing [his work on soundness, completeness, Gödel's theorem, Turing machines etc.](hhttps://aperiodical.com/2018/01/ive-re-recorded-alan-turings-can-computers-think-radio-broadcasts/) 
 
-Floyd's [obituary](http://web.stanford.edu/dept/news/pr/01/floydobit117.html) 
+Floyd's [obituary](https://cs.stanford.edu/memoriam/professor-robert-w-floyd) 
 and his seminal 1967 paper [Assigning meanings to programs](http://www.cs.berkeley.edu/~necula/Papers/FloydMeaning.pdf)
 
 Wikipedia article on [Hoare](http://en.wikipedia.org/wiki/Tony_Hoare) 
 and his seminal 1969 paper [An axiomatic basis for computer programming](http://sunnyday.mit.edu/16.355/Hoare-CACM-69.pdf)
 
 [Programming Language Constructs for Which It Is Impossible To Obtain Good Hoare Axiom Systems](http://www.cs.cmu.edu/~emc/papers/Conference%20Papers/79_impossible_hoareaxiom.pdf) by Edmund M. Clarke Jr.
-(http://www.cs.cmu.edu/~emc/papers/Conference%20Papers/79_impossible_hoareaxiom.pdf)
 
 [Zune bug](http://techcrunch.com/2008/12/31/zune-bug-explained-in-detail/) explained in detail
 
@@ -94,8 +92,8 @@ and his seminal 1969 paper [An axiomatic basis for computer programming](http://
 
 Microsoft projects:
 [SLAM](http://research.microsoft.com/en-us/projects/slam/)
-[T2 termination prover](http://research.microsoft.com/en-us/projects/t2/)
-[SLAyer](http://research.microsoft.com/en-us/projects/t2/)
+[T2 termination prover](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/04/t2-tool-report.pdf)
+[SLAyer](https://www.microsoft.com/en-us/research/publication/slayer-memory-safety-for-systems-level-code/)
 
 Wikipedia article on [Material Implication](http://en.wikipedia.org/wiki/Material_conditional) 
 the [Paradoxes of Material Implication](http://legacy.earlham.edu/~peters/courses/log/mat-imp.htm) 
@@ -105,7 +103,7 @@ Collection of [Software Bugs and Software Glitches](http://www5.in.tum.de/~huckl
 
 The VCC verifier can be downloaded from http://vcc.codeplex.com or tried at http://www.rise4fun.com/vcc
 
-Peter Homeier's [Sunrise system](http://www.cis.upenn.edu/~hol/sunrise/)
+Peter Homeier's [Sunrise system](http://www.trustworthytools.com/id13.html)
 
 [Design by Contract](http://www.eecs.ucf.edu/~leavens/JML/jmldbc.pdf) (a paper by Gary T. Leavens and Yoonsik Cheon)