Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Computer Laboratory - John Wickerson
[go: Go Back, main page]

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 particularly interested in Rely-Guarantee reasoning and separation logic.

From July to October 2011, I am an intern at European Microsoft Innovation Center in Aachen, where I am working on the VCC project. From April to July 2010, I was an intern at Microsoft Research Cambridge, where I was supervised by 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

15-Oct-2010
Unifying Models of Data Flow.
Tony Hoare and John Wickerson.
Proceedings of the 2010 Marktoberdorf Summer School (to appear).
(preprint)
05-Jan-2010
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 am 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 am supervising 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.