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.
Here is a selection of research projects I am or have been involved in.
Some hardware is designed so that each operation is performed at a set time; other hardware is designed so that each operation is performed exactly when its operands are ready. Can we combine these paradigms to obtain the best of both worlds?
FPGA 2020 TCAD 2021 FCCM 2021
Can we build a C-to-Verilog compiler that generates fast and area-efficient hardware designs and also comes with a machine-checked proof of correctness?
LATTE 2021
Can we check that C compilers are correctly implementing concurrency by feeding them random multi-threaded programs?
MET 2021
Designers of pipelined hardware have to pick an 'initiation interval' ‐ the number of clock cycles between successive inputs. What does it mean to have initiation intervals that are not integers?
ASP-DAC 2020 TCAD 2021
How can C-to-hardware compilers be extended to support C11 atomics, correctly and efficiently?
FPGA 2017 TC 2018 FCCM 2018 TVLSI 2021
In the presence of non-volatile memory, what guarantees do architectures like Intel x86 and Arm give to programmers about the order in which stores become persistent?
OOPSLA 2019 POPL 2020
Conventional compilers tend to avoid really precise pointer analyses because they make compilation take too long. But since high-level synthesis takes longer than conventional compilation anyway, is it worthwhile to use a precise pointer analysis?
FPL 2020
How much might a program running with real-time constraints on one core of a multicore processor be slowed down by a malicious program running on another core?
RTAS 2020
There are two ways to make an iterative computation more accurate: increase the number of iterations, and increase the number of decimal places being calculated. Can we build a hardware design that increases both together?
FPT 2017 ARITH 2018 TVLSI 2020
If weak memory lets memory accesses be reordered (so that more program behaviours are allowed) and transactional memory is about glueing several memory accesses together (so that fewer program behaviours are allowed), what happens if we have both at the same time?
PLDI 2018 USENIX ATC 2019
The OpenCL memory model stretches to 19 pages of dense legalese prose. Can we formalise this, with a view to providing a rigorous foundation for reasoning about the correctness of OpenCL programs and compilers?
OOPSLA 2015 POPL 2016 DHPCC++ 2018
Weak memory models abound, each subtly different. Can we use constraint-solving technology to automatically find programs that can differentiate between any two models?
POPL 2017
Can we automatically detect assertion failures, data races, and barrier divergence in programs that run on graphics processors?
IWOCL 2014 TOPLAS 2015
Mainstream CPUs are known to reorder memory accesses unless appropriate fences are used. It has been claimed that GPUs are 'infinitesimally unlikely' to expose similar behaviours. But is that really the case?
ASPLOS 2015
When conducting program proofs using the rely-guarantee method, intermediate assertions are often required to be 'stable' w.r.t. the actions of other threads. Can these stability checks be promoted from clumsy side-conditions on proof rules into first-class operators in the assertion language itself, and can this allow the rely-guarantee method to be used on library code for the first time?
ESOP 2010Conference and workshop organisation:
Program/review committee member:
Artifact evaluation committee member:
Reviewer for the following conferences and journals:
j.wickersonXimperial.ac.uk
(replace X with @)