TY - JOUR
T1 - ESBMC-GPU A context-bounded model checking tool to verify CUDA programs
AU - Monteiro, Felipe R.
AU - Da S. Alves, Erickson H.
AU - Silva, Isabela S.
AU - Ismail, Hussama I.
AU - Cordeiro, Lucas C.
AU - De Lima Filho, Eddie B.
PY - 2018/1/15
Y1 - 2018/1/15
N2 - The Compute Unified Device Architecture (CUDA) is a programming model used for exploring the advantages of graphics processing unit (GPU) devices, through parallelization and specialized functions and features. Nonetheless, as in other development platforms, errors may occur, due to traditional software creation processes, which may even compromise the execution of an entire system. In order to address such a problem, ESBMC-GPU was developed, as an extension to the Efficient SMT-Based Context-Bounded Model Checker (ESBMC). In summary, ESBMC processes input code through ESBMC-GPU and an abstract representation of the standard CUDA libraries, with the goal of checking a set of desired properties. Experimental results showed that ESBMC-GPU was able to correctly verify 85% of the chosen benchmarks and it also overcame other existing GPU verifiers regarding the verification of data-race conditions, array out-of-bounds violations, assertive statements, pointer safety, and the use of specific CUDA features.
AB - The Compute Unified Device Architecture (CUDA) is a programming model used for exploring the advantages of graphics processing unit (GPU) devices, through parallelization and specialized functions and features. Nonetheless, as in other development platforms, errors may occur, due to traditional software creation processes, which may even compromise the execution of an entire system. In order to address such a problem, ESBMC-GPU was developed, as an extension to the Efficient SMT-Based Context-Bounded Model Checker (ESBMC). In summary, ESBMC processes input code through ESBMC-GPU and an abstract representation of the standard CUDA libraries, with the goal of checking a set of desired properties. Experimental results showed that ESBMC-GPU was able to correctly verify 85% of the chosen benchmarks and it also overcame other existing GPU verifiers regarding the verification of data-race conditions, array out-of-bounds violations, assertive statements, pointer safety, and the use of specific CUDA features.
U2 - 10.1016/j.scico.2017.09.005
DO - 10.1016/j.scico.2017.09.005
M3 - Article
SN - 0167-6423
VL - 152
SP - 63
EP - 69
JO - Science of Computer Programming
JF - Science of Computer Programming
ER -