SMT-based context-bounded model checking for CUDA programs

摘要

We present ESBMC-GPU tool, an extension to the Efficient SMT-Based Context-Bounded Model Checkerrn(ESBMC), which is aimed at verifying Graphics Processing Unit (GPU) programs written for the ComputernUnified Device Architecture (CUDA) platform. ESBMC-GPU uses an operational model, that is, an abstractrnrepresentation of the standard CUDA libraries, which conservatively approximates their semantics, in orderrnto verify CUDA-based programs. It then explicitly explores the possible interleavings (up to the givenrncontext bound), while treats each interleaving itself symbolically. Additionally, ESBMC-GPU employs thernmonotonic partial order reduction and the two-thread analysis to prune the state space exploration. Experimentalrnresults show that ESBMC-GPU can successfully verify 82% of all benchmarks, while keeping lowerrnrates of false results. Going further than previous attempts, ESBMC-GPU is able to detect more propertiesrnviolations than other existing GPU verifiers due to its ability to verify errors of the program execution flowrnand to detect array out-of-bounds and data race violations.