2505

A symbolic verifier for CUDA programs

Guodong Li, Ganesh Gopalakrishnan, Robert M. Kirby, Dan Quinlan
School of Computing, University of Utah
In PPoPP ’10: Proceedings of the 15th ACM SIGPLAN symposium on Principles and practice of parallel programming (2010), pp. 357-358

@conference{li2010symbolic,

   title={A symbolic verifier for CUDA programs},

   author={Li, G. and Gopalakrishnan, G. and Kirby, R.M. and Quinlan, D.},

   booktitle={Proceedings of the 15th ACM SIGPLAN symposium on Principles and practice of parallel computing},

   pages={357–358},

   year={2010},

   organization={ACM}

}

Download Download (PDF)   View View   Source Source   

681

views

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.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2017 hgpu.org

All rights belong to the respective authors

Contact us: