Materials and links to tutorials we have given on GPUVerify and formal verification of GPU kernels.
A tutorial on how the theory, algorithms and tools of the verification community can be brought to bear on this interesting and important new domain. Aimed at researchers and practitioners in software verification who would be interested in seeing how a practical implementation of automated Hoare Logic can be built using standard components in the verification community.
A high-level introduction to GPUVerify using worked examples. Aimed at researchers and practitioners in the parallel programming community; this tutorial does not assume a background in formal verification or theoretical computer science.
A 2-hour introduction to GPUVerify that covers GPU programming, data races and barrier divergence, and the design and implementation of GPUVerify, including a demonstration of GPUVerify's verification method using a worked example. This tutorial does not assume a background in formal verification or theoretical computer science.
A more detailed tutorial on the verification method used within GPUVerify.