@@ -47,7 +47,7 @@ Recommended Reading: Mike Gordon has some [excellent notes on Hoare logic](http:
Two good books on Hoare logic are: Logic in Computer Science: Modelling and Reasoning about Systems, Michael Huth and Mark Ryan, CUP, 2004; and The Formal Semantics of Programming Languages: an Introduction, Glynn Winskel, MIT Press, 1993.
Most of the work on separation logic is in research papers.
Excellent introductions to separation logic include: O'Hearn, Reynolds and Yang's paper on [Local Reasoning about Programs that Alter Data Structures](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/localreasoning.pdf), CSL 2001, and John Reynolds' undergraduate course notes on separation logic and survey paper [Separation Logic: A Logic for Shared Mutable Data Structures](https://www.cs.cmu.edu/~jcr/seplogic.pdf), LICS 2002, both found on Reynolds' homepage.
Excellent introductions to separation logic include: O'Hearn, Reynolds and Yang's paper on [Local Reasoning about Programs that Alter Data Structures](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/localreasoning.pdf), CSL 2001, and John Reynolds' [undergraduate course notes on separation logic](http://www.cs.cmu.edu/~jcr/copenhagen08.pdf) and survey paper [Separation Logic: A Logic for Shared Mutable Data Structures](https://www.cs.cmu.edu/~jcr/seplogic.pdf), LICS 2002, both found on Reynolds' homepage.
Andrew Appel has published a book on Program Logics for Certified Compilers, CUP 2014 (a copy is available in the [library](http://www.imperial.ac.uk/admin-services/library/)).
Papers describing tool techniques include: [Symbolic Execution with Separation Logic](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.64.2006&rep=rep1&type=pdf), Berdine, Calcagno, O'Hearn, APLAS'05; [A Local Shape Analysis based on Separation Logic](http://www.eecs.qmul.ac.uk/~ddino/papers/localshape.pdf), Distefano, O'Hearn, Yang, TACAS 2006; and [Compositional Shape Analysis by Means of Bi-abduction](http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/jacm-abduction-webversion.pdf), Calcagno, Distefano, O'Hearn, Yang, JACM 2011.
