Talk "Verification of GPU kernels with VerCors"

by Marieke Huisman

Sat, 27 March 2021 at 10:40 am in Luxembourg, Luxembourg

Abstract: In this talk, I will discuss how we use permission-based separation logic to reason about GPU programs. The logic takes into account the special memory model of the GPU, where a division is made between global and local memory. Synchronisation between threads is organised by barriers and atomics, which is also catered for in the logic. I will also discuss how the VerCors annotations are encoded into Viper. Finally, I will briefly discuss some GPU verification case studies we have worked on.