News

Recent blog articles

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

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)

Talks

18-Jan-2017
Automatically Comparing Memory Consistency Models.
Delivered at POPL 2017, Paris.
(pdf, 3.6MB)
12-Jan-2017
Hardware Synthesis of Weakly Consistent C Concurrency.
Delivered at the South of England Regional Programming Language Seminar (S-REPLS), University of Oxford.
(pdf, 10.6MB)
27-Sep-2016
Automatically Comparing Memory Consistency Models.
Delivered at the South of England Regional Programming Language Seminar (S-REPLS), Imperial College London.
(pdf, 5.4MB)
20-Nov-2015
Overhauling SC atomics in C11 and OpenCL.
Delivered at the South of England Regional Programming Language Seminar (S-REPLS), Middlesex University.
(pdf, 4.7MB; YouTube video)
30-Oct-2015
Remote scope promotion: clarified, rectified, and verified.
Delivered at OOPSLA 2015, Pittsburgh.
(pdf, 5.8MB; YouTube video)
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)

Professional service

Organiser:

2015
Imperial Concurrency Workshop

Program committee member:

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

Artifact evaluation committee member:

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

External reviewer for the following conferences and journals:

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

Teaching

In the 2015/16 and 2016/17 academic years, I was a guest lecturer for the Computer Science course Models of Computation at Imperial. My slides on the Lambda Calculus, and YouTube videos of my lectures, are available here:

2015, 2016
The Lambda Calculus. (pdf, video 1, video 2, video 3)

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:

I also organised the Churchill Compsci Talks series.