Verifying CUDA programs using SMT-based context-bounded model checking
Phillipe Pereira, Higo F. Albuquerque, Hendrio Marques, Isabela Silva, Celso B. Carvalho, Lucas Carvalho Cordeiro, Vanessa Karyne Atenas dos Santos, Ricardo Ferreira · 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.