John Wickerson

John Wickerson I'm a PhD student in the Programming, Logic and Semantics Group, supervised by Matthew Parkinson and Glynn Winskel. My work focuses on logics for verifying concurrent programs. I'm currently interested in diagrammatic proof systems for Rely-Guarantee reasoning and separation logic.

From July to October 2011, I was an intern at European Microsoft Innovation Center in Aachen, where I worked on the VCC project. From April to July 2010, I was an intern at Microsoft Research Cambridge, where I was supervised by Sir Tony Hoare.

Contact details

desk
Room FS04
Computer Laboratory
William Gates Building
15 JJ Thomson Avenue
Cambridge
CB3 0FD
email
Firstname.Surname@cl.cam.ac.uk
phone
01223 763560

Publications

  1. Ribbon proofs for separation logic.
    John Wickerson, Mike Dodds and Matthew Parkinson.
    Under submission.
    (draft, Isabelle proofs)

  2. Unifying Models of Data Flow.
    Tony Hoare and John Wickerson.
    Proceedings of the 2010 Marktoberdorf Summer School on Software and Systems Safety, M. Broy et al. (Eds.), IOS Press, 2011.
    (preprint, publisher's website)

  3. Explicit Stabilisation for Modular Rely-Guarantee Reasoning.
    John Wickerson, Mike Dodds and Matthew Parkinson.
    Presented at ESOP 2010.
    (bibtex, preprint, tech report, Isabelle proofs)

Talks

15-Apr-2011
Ribbon Proofs for Separation Logic.
Delivered at the Dublin Concurrency Workshop.
(1-up pdf, 2.7MB)
25-Oct-2010
Separation Logic and Graphical Models.
Delivered at the Semantics Lunch.
(1-up pdf, 1.2MB; 6-up pdf, 1.5MB)
06-Jul-2010
A dataflow model of concurrency, communication and weak memory.
Delivered at the Cambridge Concurrency Workshop.
(1-up pdf, 213kB; 6-up pdf, 225kB)
09-Mar-2010
Explicit Stabilisation for modular Rely-Guarantee Reasoning.
Delivered at ESOP 2010.
(pdf, 1.2MB)
25-Nov-2009
Verifying malloc.
Delivered at the Northern Concurrency Workshop.
(1-up pdf, 938kB; 6-up pdf, 893kB)
26-Oct-2009
Verifying malloc using RGSep and 'Explicit Stabilisation'.
Delivered at the Semantics Lunch.
(pdf, 5.3MB)
13-May-2009
Local Rely-Guarantee Reasoning.
Delivered to the Program Verification reading group.
(pdf, 616kB)
04-Feb-2009
Automatic verification of C programs using the BLAST software model checker.
Delivered to the Program Verification reading group.
(pdf, 892kB)

Lecturing

In the 2010/11 academic year, I was a lecturer for the MPhil course Programming Logics and Software Verification. The slides presented in my lectures are available here:
8-Feb-2011
Lecture 6. More Separation Logic. (pdf, 1.6MB)
8-Mar-2011
Lecture 14. Rely-Guarantee (pdf, 504kB)
10-Mar-2011
Lecture 15. RGSep (pdf, 1MB)

Supervising

In the 2010/11 academic year, I supervised the following Computer Science Tripos courses:

In previous years I have supervised:

I supervise for Churchill College, where I also organise the Churchill Compsci Talks series.

And finally...

I have a personal blog at johnwickerson.wordpress.com.