Videos recorded by Alastair Donaldson about GPUVerify.
This first video gives an overview of GPUVerify, including a demonstration of the tool in action on some practical examples.
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.
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.