Verifying CUDA Programs using SMT-Based Context-Bounded Model Checking
Federal University of Amazonas
ACM Symposium on Applied Computing (SAC), 2016
@article{pereira2016verifying,
title={Verifying CUDA Programs using SMT-Based Context-Bounded Model Checking},
author={Pereira, Phillipe A and Albuquerque, Higo F and Marques, Hendrio M and Silva, Isabela S and Carvalho, Celso B and Cordeiro, Lucas C},
year={2016}
}
We present ESBMC-GPU, an extension to the ESBMC model checker that is aimed at verifying GPU programs written for the CUDA framework. ESBMC-GPU uses an operational model for the verification, i.e., an abstract representation of the standard CUDA libraries that conservatively approximates their semantics. ESBMC-GPU verifies CUDA programs, by explicitly exploring the possible interleavings (up to the given context bound), while treating each interleaving itself symbolically. Experimental results show that ESBMC-GPU is able to detect more properties violations, while keeping lower rates of false results.
January 7, 2016 by hgpu
