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


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.