ESBMC-GPU A context-bounded model checking tool to verify CUDA programs

• Published in: Science of computer programming 2018-01, Vol.152, p.63-69
• Main Authors: Monteiro, Felipe R., da S. Alves, Erickson H., Silva, Isabela S., Ismail, Hussama I., Cordeiro, Lucas C., de Lima Filho, Eddie B.
• Format: Article
• Language: English
• Subjects: CUDA; Formal verification; GPU verification; Model checking
• ISSN: 0167-6423; 1872-7964
• DOI: 10.1016/j.scico.2017.09.005

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. •ESBMC-GPU marks the first application of an SMT-based context-BMC tool for CUDA programs.•ESBMC-GPU prunes space-state exploration through state hashing and partial order reduction.•ESBMC-GPU presents improved ability to detect array out-of-bounds and data race violations.