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
John Wickerson
[go: Go Back, main page]

John Wickerson

John Wickerson 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.

Contact details

email
j.wickersonXimperial.ac.uk (replace X with @)
mail
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)

Drafts

  1. GPU concurrency: weak behaviours and programming assumptions. new
    Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen and John Wickerson.
    Under submission.

  2. Partial and total correctness as greatest and least fixed points. new
    John Wickerson.
    Draft, June 2014.
    (pdf)

  3. The Design and Implementation of a Verification Technique for GPU Kernels. new
    Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson and John Wickerson.
    Under submission.

  4. Ribbon proofs and dynamically-scoped quantifiers.
    John Wickerson.
    Rough draft, April 2013.
    (pdf)

Publications

  1. 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)

  2. Syntax and semantics of a GPU kernel programming language.
    John Wickerson.
    Archive of Formal Proofs, 2014.
    (entry, proof document, html version)

  3. Ribbon proofs.
    John Wickerson.
    Archive of Formal Proofs, 2013.
    (entry, proof document, html version)

  4. Ribbon proofs for separation logic.
    John Wickerson, Mike Dodds and Matthew Parkinson.
    Proceedings of ESOP 2013.
    (preprint, publisher's version)

  5. Ribbon proofs for separation logic.
    John Wickerson, Mike Dodds and Matthew Parkinson.
    Short paper at LICS 2012.
    (preprint, slides)

  6. 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)

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

Thesis

  1. Concurrent Verification for Sequential Programs.
    John Wickerson.
    PhD thesis, University of Cambridge, 2013.
    (tech report)

Software

  1. The ribbonproofs package.
    John Wickerson
    LaTeX package, July 2013.
    (package on CTAN, pdf manual on CTAN)

Talks

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)

Teaching

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:

and I also organised the Churchill Compsci Talks series.

And finally...

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