The tutorial will not assume that the audience has read any background
material on formal analysis techniques for GPU kernels. Nevertheless,
some advance preparation is likely to make the tutorial material
easier to follow.
The tutorial will, in part, cover material from the following paper:
Other relevant recent works on verification and semantics for GPU
- G. Li, P. Li, G. Sawaya, G. Gopalakrishnan, I. Ghosh, and S.P. Rajan. GKLEE: concolic verification and test generation for GPUs. In PPOPP 2012.
- G. Li, G. Gopalakrishnan. Scalable SMT-based
verification of GPU kernel functions. In FSE 2010.
- P. Collingbourne, C. Cadar, P.H.J. Kelly. Symbolic testing of
OpenCL code. In HVC 2011.
- A. Leung, M. Gupta, Y. Agarwal, R. Gupta, R. Jhala, S. Lerner. Verifying GPU
kernels by test amplification. PLDI 2012.
- A. Habermaier, A. Knapp. On the correctness of the SIMT execution model of GPUs. In ESOP 2012.