Mar 05, 2013: Matej Mihelčić: Specification and Verification of GPGPU Programs using Permission-Based Separation Logic

March 05, 2013Specification and Verification of GPGPU Programs using Permission-Based Separation Logic
Room: Zi 5126Matej Mihelčić
12:30-13:30

Graphics processing units (GPUs) are increasingly used in general purpose computing. They are available, relatively cheap, energy efficient and provide enormous computing power. 
Since they are used to solve various scientific and industrial task, there is a need to to develop approaches and tools to prove correctness of GPU programs. 
In this presentation we will shortly describe memory and execution model of OpenCL, a standard for heterogeneous parallel computing. Following, we will introduce main advantages of using permission-based separation logic and demonstrate our ideas of applying this logic to verification of GPU kernels. Finally, we will demonstrate this approach on several examples.