GPUVerify with Barrier Invariants

This webpage accompanies our OOPSLA 2013 paper.

GPUVerify is a tool for verifying race- and divergence-freedom of OpenCL and CUDA kernels. Our paper presents an extension to GPUVerify for reasoning about thread interactions using Barrier Invariants. This allows us to verify data-dependent GPU kernels.

For reproducibility, we give binaries and code for our toolchain and experimental evaluation for the Blelloch, Brent Kung and Kogge Stone prefix sum algorithms discussed in the paper.


We recommend you download the artifact, that we prepared for the OOPSLA Artifact Evaluation Committee, which contains a VirtualBox virtual machine image with all the required dependencies installed.

NB: the Linux downloads additionally require glibc 3.4.15 and mono 3.0.4 to be installed.