Formal Analysis Techniques for GPU Kernels
Tutorial at HiPEAC 2014, Berlin
21 January 2014


December 2013

FAT-GPU web site goes live.

July 2013

FAT-GPU is accepted as a half-day tutorial at HiPEAC 2014.


FAT-GPU 2014 is supported by the FP7 project CARP: Correct and Efficient Accelerator Programming

The tutorial is also supported by the HiPEAC Network of Excellence, through which the HiPEAC conference is organised.


The FAT-GPU 2014 tutorial will be held as part of the HiPEAC 2014 conference.


  • 10:00-10:30 Brief overview of GPU programming, data races and barrier divergence
  • 10:30-11:00 Demo of GPUVerify, showing how it can be used to analyse a variety of kernels, and illustrating the tool's strengths and weaknesses

  • 11:00-11:30 Break

  • 11:30-12:00 Details of the GPUVerify tool chain
  • 12:00-12:30 Overview of the GPUVerify verification method, focussing on scalability to large numbers of threads
  • 12:30-13:00 Showcase of ongoing work on the project, including formalisation of the OpenCL 2.0 memory model