A symbolic verifier for CUDA programs
Guodong Li, Ganesh Lalitha Gopalakrishnan, Robert M. Kirby, Dan Quinlan · 2010
We present a preliminary automated verifier based on mechanical decision procedures which is able to prove functional correctness of CUDA programs and guarantee to detect bugs such as race conditions. We also employ a symbolic partial order reduction (POR) technique to mitigate the interleaving explosion problem.