John Wickerson

John Wickerson

I'm a Lecturer in the Circuits and Systems group, which is part of the Department of Electrical and Electronic Engineering at Imperial College London.

My research aims to improve the reliability of high-performance computing with the help of formal methods.

My latest project investigates the interaction between transactions and weak memory. I have previously worked on compiling weakly-consistent concurrent software into hardware, on generating test-cases for memory consistency models, on formalising the concurrency semantics of C/C++ and OpenCL, on diagrammatic proofs about programs, and on software verification using the rely/guarantee method.

News

Recent blog articles

29-Jun-2018
Greatest Hits of PLDI 2018
6-May-2018
What is the difference between latency and throughput?
4-May-2018
Greatest Hits of FCCM 2018
5-Mar-2018
Concurrency-aware scheduling for high-level synthesis
12-Feb-2018
What do you get if you cross Weak Memory with Transactional Memory?
15-Aug-2017
Who has the most POPL and PLDI papers?
22-Jul-2017
Who has the most FPGA, FCCM, FPL, and FPT papers?
17-Apr-2017
Ribbon Diagrams for Weak Memory
23-Feb-2017
Translating lock-free, relaxed concurrency from software into hardware
11-Nov-2016
Memory Consistency Models, and how to compare them automatically
11-Aug-2016
cppreference.com gets acquire/release instructions wrong
6-Aug-2016
Why we should plot normalised data on a logarithmic scale

Publications

Journal articles

Conference papers

Book chapters

Other publications

People

Team

Collaborators

Unpublished notes

  1. Partial and total correctness as greatest and least fixed points.
    John Wickerson.
    (pdf, Isabelle proofs)

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

  3. Nominal Prolog.
    John Wickerson (supervised by Andrew Pitts).
    Third-year (Part II) dissertation, University of Cambridge, 2008.
    (pdf)

Professional service

Program committee member:

2019
ACM Int. Conf. on Programming Lang. Design and Implementation (PLDI)
Asia and South Pacific Design Automation Conference (ASP-DAC)
Designer Track, Design Automation Conference (DAC)
2018
Reengineering for Parallelism in Heterogeneous Parallel Platforms (RePara)
Designer Track, Design Automation Conference (DAC)
Field-Programmable Logic and Applications (FPL)
2017
Field-Programmable Logic and Applications (FPL)
2016
Reengineering for Parallelism in Heterogeneous Parallel Platforms (RePara)
Tiny Transactions on Computer Science (TinyTOCS)
2015
Automated Verification of Critical Systems (AVoCS)
Reengineering for Parallelism in Heterogeneous Parallel Platforms (RePara)

External review committee member:

2019
Europ. Conf. on Object-Oriented Programming (ECOOP)

Artifact evaluation committee member:

2015
ACM Symp. on Principles of Programming Languages (POPL)

External reviewer for the following conferences and journals:

2018
IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems (TCAD)
IEEE Int. Symp. on Field-Programmable Custom Computing Machines (FCCM)
IEEE Int. Conf. on Software Testing, Verification and Validation (ICST)
ACM Int. Conf. on Programming Lang. Design and Implementation (PLDI)
2017
ACM/SIGDA Int. Symp. on Field-Programmable Gate Arrays (FPGA)
Journal of Supercomputing
Symp. on Parallelism in Algorithms and Architectures (SPAA)
2016
ACM Trans. on Computational Logic (TOCL)
ACM Trans. on Reconfigurable Technology and Systems (TRETS)
ACM Int. Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)
ACM Symp. on Principles of Programming Languages (POPL)
ACM Symp. on Principles and Practice of Parallel Programming (PPoPP)
2015
Int. Conf. on Computer Aided Verification (CAV)
Europ. Symp. on Programming (ESOP)
ACM Symp. on Principles of Programming Languages (POPL)
ACM Symp. on Principles and Practice of Parallel Programming (PPoPP)
2014
Joint Int. Conf. on Rewriting and Typed Lambda Calculi (RTA-TLCA)
Int. Conf. on Runtime Verification (RV)
Static Analysis Symp. (SAS)
2012
ACM Int. Conf. on Certified Programs and Proofs (CPP)
Int. Conf. on Relational and Algebraic Methods in Computer Science (RAMiCS)
Symp. on Parallelism in Algorithms and Architectures (SPAA)
Int. Conf. on Verified Software: Theories, Tools, and Experiments (VSTTE)
2011
Int. Conf. on Computer Aided Verification (CAV)
2010
Europ. Symp. on Programming (ESOP)
ACM/IEEE Symp. on Logic in Computer Science (LICS)
ACM Symp. on Principles of Programming Languages (POPL)
Int. Conf. on Verified Software: Theories, Tools, and Experiments (VSTTE)
2009
ACM Int. Conf. on Programming Lang. Design and Implementation (PLDI)

Organiser:

2015
Imperial Concurrency Workshop

Lectures and Seminars

Sep 2018
Towards Verified Hardware Compilation.
Presented at the Sixth Workshop on Formal Methods and Tools for Security (FMATS).
(pdf)
May 2018
Journey to the Centre of the OpenCL Memory Model.
Keynote address to the Workshop on Distributed and Heterogeneous Programming in C and C++ (DHPCC++).
(pdf)
Dec 2016
The Lambda Calculus.
Three guest lectures as part of the Models of Computation course at Imperial.
(pdf, video 1, video 2, video 3)
Nov 2014
Ribbon Proofs for Separation Logic.
A guest lecture as part of the Separation Logic course at Imperial.
(pdf)
Mar 2014
Verifying heap-manipulating programs using Separation Logic.
A guest lecture as part of the Software Reliability course at Imperial.
(pdf)
Mar 2014
Verifying concurrent programs using Rely/Guarantee and Separation Logic.
A guest lecture as part of the Software Reliability course at Imperial.
(pdf)
Feb 2014
Automatic Verification of GPU kernels.
A guest lecture as part of the Hoare Logic course at Cambridge.
(pdf)
Jan 2014
Formal Analysis Techniques for GPU kernels.
A tutorial at the HiPEAC '14 conference about the GPUVerify tool developed in the Multicore Group at Imperial.
(pdf)
Jan 2014
A Very Rough Introduction to Linear Logic.
A seminar to the Multicore group.
(pdf)
Nov 2013
Nominal Unification.
A seminar to the Multicore group.
(pdf)
Jan 2013
A graphical introduction to Separation Logic.
Two guest lectures as part of the Quality Assurance of Embedded Systems course at TU Berlin.
(pdf)
Feb 2011
Rely-Guarantee and Separation Logic.
Three guest lectures as part of the Programming Logics and Software Verification course at Cambridge.
(lecture 1, lecture 2, lecture 3)
May 2009
Local Rely-Guarantee Reasoning.
A seminar to the Program Verification reading group.
(pdf)
Feb 2009
Automatic verification of C programs using the BLAST software model checker.
A seminar to the Program Verification reading group.
(pdf)