Verifying CUDA Programs using SMT-Based Context-Bounded Model Checking

Phillipe A. Pereira, Higo F. Albuquerque, Hendrio M. Marques, Isabela S. Silva, Celso B. Carvalho, Lucas C. Cordeiro
Federal University of Amazonas
ACM Symposium on Applied Computing (SAC), 2016


   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},



Download Download (PDF)   View View   Source Source   Source codes Source codes




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.
Rating: 2.5/5. From 1 vote.
Please wait...

* * *

* * *

HGPU group © 2010-2021 hgpu.org

All rights belong to the respective authors

Contact us: