GPUVerify: an Approach to Automated Verification of GPU Kernels

Alastair Donaldson

I will present an overview of the GPUVerify project, a collaboration between the Multicore Programming group at Imperial College London and Shaz Qadeer at the RiSE group, Microsoft Research Redmond. The aim of the project has been to design a highly automatic method for proving a key correctness property -- data race-freedom -- for software designed to run on graphics processing units. In the talk I will give a brief overview of GPUs and the GPU programming model, and will demo the GPUVerify tool in action on some practical examples. I will then present an overview of the core theoretical ideas on which the tool is based, and I will show how the verification conditions that establish correctness of a GPU program are encoded in the Boogie intermediate verification language.

Alastair Donaldson is a Senior Lecturer in the Department of Computing, Imperial College London, where he leads the Multicore Programming Group and is Coordinator of the FP7 project CARP: Correct and Efficient Accelerator Programming. He has published more than 50 peer-reviewed papers in formal verification and multicore programming, and leads the GPUVerify project on automatic verification of GPU kernels, which is a collaboration with Microsoft Research. Before joining Imperial, Alastair was a Visiting Researcher at Microsoft Research Redmond, a Research Fellow at the University of Oxford and a Research Engineer at Codeplay Software Ltd. He holds a PhD from the University of Glasgow.