Research

Research Outline

I am interested in automated techniques for helping developers to write reliable software that runs efficiently on modern hardware.

Formal verification techniques for multicore software. I am especially interested in lightweight, automatic formal verification techniques, capable of operating directly on source code, that can be implemented as efficient tools to be used in day-to-day software development.

My current research in this area is on finding bugs, or proving correctness, of graphics processing unit (GPU) kernels. The techniques I and my research group are working on, in collaboration with Shaz Qadeer, have led to the design and implementation of GPUVerify, a practical tool for analysis of GPU kernels. This work uses automated theorem provers and invariant inference techniques, and is implemented using the LLVM/CLANG and Boogie frameworks.

More generally, I am interested in formal analysis techinques for concurrent software. With colleagues formerly at the Univeristy of Oxford in the group of Prof Daniel Kroening (and now scattered across the world!) I have designed various analysis techniques related to concurrency; see the papers below.

Software performance optimization for multicore processors. To take advantage of modern multicore processors, we need suitable abstractions to allow programmers to write high-level, portable programs, from which efficient parallel code can be generated. I got interested in this area while working as a Research Engineer at Codeplay Software Ltd. This is a key focus for the CARP project, which I am coordinating.

Selected Papers

List of all my papers

Tools