This website accompanies our CAV 2014 submission. GPUVerify is a tool for verifying race- and divergence-freedom of OpenCL and CUDA kernels. Our paper reports on our practical experiences over the last 2.5 years related to the engineering of GPUVerify. In particular, we describe the progress of GPUVerify from a research prototype to a fully functional and relatively efficient analysis tool.

As part of our paper, we evaluate our optimisations over a set of 564 GPU kernels. For reproducibility, we give binaries and code for our toolchain and experimental evaluation.

If you need help with our artifact then please email Nathan.


GPUVerify is given as a binary for Linux or Windows (64-bit). GPUVerify requires python and additionally, for Linux, mono ≥ 3.0.7. There is a regression inside the tarball that you should make sure passes on your local machine. We give 502 kernels used in our experimental evaluation tarball (we exclude 62 kernels from the commercial Rightware suite). Instructions and scripts for reproducing our experimental results are included. Finally, we give the raw data we generated on our machines, which we used to generate the tables and graphs in our paper.

Interactive plots

We reproduce our scatter plot graphs (Figures 2a and 2b) as interactive plots so that you can explore the data.

Breakdown of kernels given in paper

Our paper studies 564 kernels, broken down as follows:

All kernels, except for the commercial Rightware Basemark CL kernels, are included in the download above. Across all the optimisations that we discuss in our paper, we breakdown the kernels into the following sets: