A formal verification tool for proving correctness properties of GPU kernels written in OpenCL and CUDA

Overview

GPUVerify is a formal verification tool that uses verification condition generation and automated theorem proving to prove correctness properties of, or find defects in, GPU kernels written in the OpenCL and CUDA languages. For further details check out the GPUVerify home page, and look at the source code on GitHub.

Research Support

This research has been supported by the EU FP7 CARP project, Correct and Efficient Accelerator Programming, EPSRC project EP/K011499/1, Scalable Automatic Verification of GPU Kernels, an EPSRC Pathways to Impact Award, the Imperial College UROP scheme, a gift from Intel Corporation. The project commenced when Alastair Donaldson was a Visiting Researcher at Microsoft Research Redmond.

Publications

• The Design and Implementation of a Verification Technique for GPU Kernels

  Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson, John Wickerson

  ACM Transactions on Programming Languages and Systems

• The GPUVerify Method: a Tutorial Overview

  Alastair F. Donaldson

  ECEASST

• Engineering a Static Verification Tool for GPU Kernels

  Ethel Bardsley, Adam Betts, Nathan Chong, Peter Collingbourne, Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema, Daniel Liew, Shaz Qadeer

  26th International Conference on Computer Aided Verification (CAV'14)

• KernelInterceptor: Automating GPU Kernel Verification by Intercepting Kernels and their Parameters

  Ethel Bardsley, Alastair F. Donaldson, John Wickerson

  International Workshop on OpenCL (IWOCL'14)

• Warps and Atomics: Beyond Barrier Synchronization in the Verification of GPU Kernels

  Ethel Bardsley, Alastair F. Donaldson

  6th International NASA Formal Methods Symposium (NFM'14)

• A Sound and Complete Abstraction for Reasoning About Parallel Prefix Sums

  Nathan Chong, Alastair F. Donaldson, Jeroen Ketema

  41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'14)

• Barrier Invariants: a Shared State Abstraction for the Analysis of Data-Dependent GPU Kernels

  Nathan Chong, Alastair F. Donaldson, Paul H. J. Kelly, Jeroen Ketema, Shaz Qadeer

  28th Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'13)

• GPUVerify: a Verifier for GPU Kernels

  Adam Betts, Nathan Chong, Alastair F. Donaldson, Shaz Qadeer, Paul Thomson

  27th Annual {ACM} {SIGPLAN} Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'12)