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. My work focuses on logics for verifying concurrent programs. I'm particularly interested in Rely-Guarantee reasoning and separation logic.

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

05-Jan-2010
Explicit Stabilisation for Modular Rely-Guarantee Reasoning.
With Mike Dodds and Matthew Parkinson. Presented at ESOP 2010.
(bibtex, preprint, Isabelle proofs)

Talks

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)

Supervisions

In the 2009/10 academic year I will be 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.

Miscellaneous

09-Mar-2010
Installing LaTeX fonts on Mac OS X (for use in Keynote, etc.) - this tip worked for me!
07-Jan-2010
The MathUnicode keyboard layout (and using it with LaTeX) (pdf documentation, sample LaTeX file, keylayout, LaTeX style file)
04-Jan-2010
A little theorem about odd powers (pdf)
25-Nov-2009
Partial and total correctness as greatest and least fixpoints(pdf)
19-Nov-2009
Source code of Doug Lea's malloc (1-up pdf, 2-up pdf)
26-Oct-2009
My attempt at a wifi logo (inspired by this t-shirt) (png)
16-Mar-2009
Concurrent Buns: A Chef's Guide to Concurrency Verification (pdf, html)
24-Feb-2009
The johnproof LaTeX environment (LaTeX style file, pdf documentation)
04-Feb-2009
A new notation for building sets? (pdf)
26-Jan-2009
Does lub-preservation imply monotonicity? (pdf)
22-Jan-2009
Implementing difference lists in Prolog (pdf, html)
02-May-2008
Nominal Prolog (my third-year undergraduate project) (pdf, 948kB)