Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels

DOI10.1007/978-3-642-37036-6_16zbMath1381.68139OpenAlexW2156138494MaRDI QIDQ5326291

Alastair F. Donaldson, Peter Collingbourne, Jeroen Ketema, Shaz Qadeer

Publication date: 5 August 2013

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-37036-6_16

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55)

Related Items (4)

A Hoare Logic for GPU Kernels ⋮ Checking data-race freedom of GPU kernels, compositionally ⋮ A Hoare Logic for SIMT Programs ⋮ GPUVerify

Uses Software

• CUDA
• OpenCL
• Boogie
• GKLEE

This page was built for publication: Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels