I'm a postdoctoral researcher in the Multicore Group, which is part of the Department of Computing at Imperial College London.

My current research concerns programming with GPUs, and I am specifically interested in formalising the memory model defined by the OpenCL standard.

In previous research, I have developed a diagrammatic proof system for separation logic, and I have investigated the application of the rely-guarantee method to the verification of sequential modules.

`j.wickersonXimperial.ac.uk`

(replace`X`

with @)- John Wickerson

Department of Computing

Huxley Building

180 Queens Gate

London

SW7 2RH - desk
- Room 213,

William Penney Laboratory

(getting to the campus, map of the campus)

*Taming the complexities of the C11 and OpenCL memory models*.

John Wickerson and Mark Batty.

Under submission, Jan 2015.

(pdf)

*Partial and total correctness as greatest and least fixed points*.

John Wickerson.

Under submission, Jan 2015.

(pdf, Isabelle proofs)*The Design and Implementation of a Verification Technique for GPU Kernels*.

Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson and John Wickerson.

Under submission.*Ribbon proofs and dynamically-scoped quantifiers*.

John Wickerson.

Rough draft, April 2013.

(pdf)

*GPU concurrency: weak behaviours and programming assumptions*.

Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen and John Wickerson.

Proceedings of ASPLOS 2015. To appear.

(preprint)*KernelInterceptor: Automating GPU kernel verification by intercepting kernels and their parameters*.

Ethel Bardsley, Alastair F. Donaldson and John Wickerson.

In Proceedings of IWOCL 2014.

(preprint)*Syntax and semantics of a GPU kernel programming language*.

John Wickerson.

Archive of Formal Proofs, 2014.

(entry, proof document, html version)*Ribbon proofs*.

John Wickerson.

Archive of Formal Proofs, 2013.

(entry, proof document, html version)*Ribbon proofs for separation logic*.

John Wickerson, Mike Dodds and Matthew Parkinson.

Proceedings of ESOP 2013.

(preprint, publisher's version)*Ribbon proofs for separation logic*.

John Wickerson, Mike Dodds and Matthew Parkinson.

Short paper at LICS 2012.

(preprint, slides)*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 version)*Explicit Stabilisation for Modular Rely-Guarantee Reasoning*.

John Wickerson, Mike Dodds and Matthew Parkinson.

Proceedings of ESOP 2010.

(preprint, publisher's version, tech report, Isabelle proofs)

*Concurrent Verification for Sequential Programs*.

John Wickerson.

PhD thesis, University of Cambridge, 2013.

(tech report)

*The*.`ribbonproofs`

package

John Wickerson

LaTeX package, July 2013.

(package on CTAN, pdf manual on CTAN)

- 28-Apr-2014
*Tools for exploring and understanding memory models*.

Delivered at the York Concurrency Workshop.

(pdf, 1.5MB)- 07-Jan-2014
*A Very Rough Introduction to Linear Logic*.

Delivered at the Multicore group seminar.

(pdf, 364kB)- 05-Nov-2013
*Nominal Unification*.

Delivered at the Multicore group seminar.

(pdf, 349kB)- 20-Mar-2013
*Ribbon Proofs for Separation Logic*.

Delivered at ESOP 2013.

(pdf, 11.2MB)- 27-Jun-2012
*Ribbon Proofs for Separation Logic*.

Delivered at LICS 2012.

(pdf, 1.3MB)- 15-Apr-2011
*Ribbon Proofs for Separation Logic*.

Delivered at the Dublin Concurrency Workshop.

(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)

In the 2014/15 academic year, I was a guest lecturer for the Computer Science course Separation Logic at Imperial. The slides presented in my lectures are available here:

- 18-Nov-2014
*Ribbon Proofs for Separation Logic.*(pdf, 7.3MB)

In the 2013/14 academic year, I was a guest lecturer for the Computer Science course Software Reliability at Imperial. The slides presented in my lectures are available here:

- 04-Mar-2014
- Lecture 16.
*Verifying heap-manipulating programs using Separation Logic.*(pdf, 2.1MB) - 06-Mar-2014
- Lecture 17.
*Verifying concurrent programs using Rely/Guarantee and Separation Logic.*(pdf, 1.6MB)

In the 2013/14 academic year, I was a guest lecturer for the Part II Computer Science course Hoare Logic at Cambridge. The slides presented in my lecture are available here:

- 11-Feb-2014
- Lecture 8.
*Automatic Verification of GPU kernels.*(pdf, 594kB)

I gave a tutorial at the HiPEAC '14 conference about the GPUVerify tool developed here in the Multicore Group at Imperial.

- 21-Jan-2014
*Formal Analysis Techniques for GPU kernels.*(pdf, 627kB)

In the 2012/13 academic year, I was a guest lecturer for the graduate course Quality Assurance of Embedded Systems at TU Berlin. The slides presented in my lectures are available here:

- 15-Jan-2013
*A graphical introduction to Separation Logic (Part I).*(pdf - both lectures, 364kB)- 22-Jan-2013
*A graphical introduction to Separation Logic (Part II).*

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)

At Cambridge, I supervised several courses:

- Denotational Semantics,
- Discrete Mathematics II,
- Hoare Logic,
- Foundations of Functional Programming,
- Prolog,
- Semantics of Programming Languages,
- Specification and Verification I,
- Topics in Concurrency, and
- Types,

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