GPUVerify: a technique for formal verification of GPU kernels
- 16:00 7th November 2013 ( week 4, Michaelmas Term 2013 )278
I will report on recent work in the Multicore Programming Group at Imperial on the verification of data parallel programs. The principal focus of the talk will be on GPUVerify, a verification technique and tool for GPU kernels written in OpenCL and CUDA. This project started when I was a Visiting Researcher at MSR during 2011, and has evolved into a now fairly usable tool which we are pushing to GPU programmers. GPUVerify achieves scalability by transforming a massively parallel GPU kernel into a sequential program that can be checked using existing theorem-proving based tools such as Microsoft's Boogie. I will describe how this transformation works, discuss practical issues associated with building a tool chain that can operate directly on OpenCL and CUDA source code, and describe recent developments related to improving the efficiency of invariant inference. For an introduction to GPUVerify see:
- http://www.youtube.com/watch?v=l8ysBPV8OvA
- http://rise4fun.com/GPUVerify-OpenCL