GPUVerify: Formal Analysis Tool for OpenCL and CUDA Kernels
GPUVerify is a command line tool that allows formal analysis of GPU kernels written in OpenCL and CUDA.
GPUVerify can detect intra-group data races (in OpenCL, it’s a race between work items in the same work group), inter-group data races (in OpenCL, it’s a race between work items in different work groups), barrier divergence (barrier synchronization).
GPUVerify is available for Windows 7/8 64-bit and for Linux 64-bit and requires Python 2.7. You can download GPUVerify from THIS PAGE.