A symbolic verifier for CUDA programs
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}
}
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.
January 16, 2011 by hgpu
