I'm a postdoctoral research associate working with George Constantinides in the Circuits and Systems group, which is part of the Department of Electrical and Electronic Engineering at Imperial College London.

My latest research project involves improving the semantics of atomic operations in C11 and OpenCL. I have
previously worked on a detailed
study of AMD's *remote-scope promotion* technology, on diagrammatic proofs of program
correctness using separation logic, and on modular verification using the
rely-guarantee method.

`j.wickersonXimperial.ac.uk`

(replace`X`

with`@`

)- Dr John Wickerson

Department of Electrical and Electronic Engineering

Imperial College London

South Kensington Campus

London

SW7 2AZ - desk
- Room 905

9th Floor

Department of Electronic and Electrical Engineering

(getting to the campus, map of the campus)

I organise the weekly meetings of the *Memory and
Synthesis* sub-group (iCalendar schedule).

See also my DBLP entry.

*Remote-scope promotion: clarified, rectified, and verified*.

**John Wickerson**, Mark Batty, Alastair F. Donaldson and Bradford M. Beckmann.

Accepted for publication at OOPSLA 2015.

(preprint)

*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**.

TOPLAS, 37(3), May 2015.

(preprint, publisher's version, Isabelle formalisation in the Archive of Formal Proofs)*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**.

In proceedings of ASPLOS 2015.

(preprint, project page)*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, publisher's version)*Ribbon proofs for separation logic*.**John Wickerson**, Mike Dodds and Matthew Parkinson.

Proceedings of ESOP 2013.

(preprint, publisher's version, Isabelle formalisation in the Archive of Formal Proofs)*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 (supervised by Matthew Parkinson, Mike Dodds and Glynn Winskel).

PhD thesis, University of Cambridge, 2012.

(tech report)*Nominal Prolog*.

John Wickerson (supervised by Andrew Pitts).

Third-year (Part II) dissertation, University of Cambridge, 2008.

(pdf)

*Automatically Optimizing the Latency, Area, and Accuracy of C Programs for High-Level Synthesis*.

Under submission, Jul 2015.*Custom-Sized Caches in Application-Specific Memory Hierarchies*.

Under submission, Jul 2015.*Overhauling SC atomics in C11 and OpenCL*.

Under submission, Jul 2015.

(pdf)

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

Under submission.

(pdf, Isabelle proofs)*Ribbon proofs and dynamically-scoped quantifiers*.**John Wickerson**.

Rough draft, April 2013.

(pdf)

*Herd - a generic memory model simulator*.

John Wickerson, contributor (Aug 2014 ‐ Jan 2015).

(source code on GitHub)*The*.`ribbonproofs`

package

John Wickerson

LaTeX package, July 2013.

(package on CTAN, pdf manual on CTAN)

- 15-Jul-2015
*Overhauling SC atomics in C11 and OpenCL*.

Delivered at the Imperial Concurrency Workshop.

(pdf, 4.9MB)- 22-Apr-2015
*Remote scope promotion: clarified, rectified, and verified*.

Delivered at the REMS workshop, Cambridge.

(pdf, 4.1MB)- 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)

Organiser:

- Imperial Concurrency Workshop, July 2015.

Program committee member:

- AVoCS '15
- RePara '15

Artifact evaluation committee member:

- POPL '15

External reviewer for submissions to the following conferences:

- PLDI '09
- POPL '10
- ESOP '10
- LICS '10
- VSTTE '10
- CAV '11
- VSTTE '12
- SPAA '12
- RAMiCS '12
- CPP '12
- RTATLCA '14
- SAS '14
- RV '14
- POPL '15
- PPOPP '15
- ESOP '15
- CAV '15

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
- Types