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 shall be doing an internship at Microsoft Research Cambridge, 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

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, 6-up pdf)
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)