GPUVerify: a Verifier for GPU Kernels


Videos recorded by Alastair Donaldson about GPUVerify.

Introduction and overview

This first video gives an overview of GPUVerify, including a demonstration of the tool in action on some practical examples.

Verification method

This second video explains how the verification techniques of GPUVerify works under the hood, showing how data race analysis for a massively parallel kernel can be reduced to analysis of a sequential program.

Predicated execution and invariant inference

In the final video Alastair covers two advanced topics: the lock-step predicated execution technique that the tool uses to handle conditional and looping code, and the manner by which loop invariants are automatically inferred using the Houdini algorithm.