I am currently a researcher for ARM, where I work on hardware and software at many levels of the system stack. My research interests are parallel programming, computer architecture and formal reasoning. Specifications and problems at the hardware/software boundary get me excited. My previous work in this area include proofs of correctness for cache-coherence protocols, memory models and formalising architectural specifications. My PhD focused on scalable verification techniques for data-parallel programs.
I was very fortunate to take part in the EPSRC ICT Pioneers 2014 competition. The core message of my talk was about the need and opportunity for static verification to provide powerful tools to help programmers write better programs. For more information about GPUVerify check out our main webpage and these introductory tutorials and videos.
I am a key contributor to GPUVerify, a verification technique and tool for the automatic analysis of GPU kernels written in OpenCL and CUDA. At ARM, prior to my PhD, I developed prototypes and tools for CPU virtualisation (now found in the ARMv7 architecture), cache coherence verification (now in AMBA4 ACE) and instruction set simulators (the Cortex-M1 simulator shipped in RVDS).
I am an advocate of repeatable and reproducible research that enables other researchers to build upon my work. The accompanying artifact to my OOPSLA'13 paper was approved by the OOPSLA evaluation committee and allows others to use GPUVerify and repeat the experimental evaluation given in my paper. I served on the PLDI 2014 artifact evaluation committee and POPL 2015 artifact evaluation committee.
Implementing and Evaluating Candidate-Based Invariant Generation, arxiv coRR, 2016
The Design and Implementation of a Verification Technique for GPU Kernels, ACM Transactions on Programming Languages and Systems, 2015
Many-Core Compiler Fuzzing, ACM SIGPLAN Conference on Programming Language Design and Implementation, 2015
Engineering a Static Verification Tool for GPU Kernels, Computer Aided Verification, 2014
A Sound and Complete Abstraction for Reasoning about Parallel Prefix Sums, ACM SIGPLAN Symposium on Principles of Programming Languages, 2014
Barrier Invariants: a Shared State Abstraction for the Analysis of Data-Dependent GPU Kernels, ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2013
GPUVerify: a Verifier for GPU Kernels, ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2012
IP Modeling and Verification, Book chapter in Processor and System-on-Chip Simulation (Springer), 2010
Stream Compilation for Real-Time Embedded Multicore Systems, IEEE/ACM International Symposium on Code Generation and Optimization, 2009
Reasoning about the ARM weakly consistent memory model, ACM SIGPLAN Workshop on Memory Systems Performance and Correctness, 2008
The ARMv6M Architecture in Coq, Workshop on Hardware Design and Functional Languages, 2007