ESBMC-GPU

A context-bounded model checker based on SMT to verify CUDA programs for data races, deadlocks, and other properties.

ESBMC-GPU is a context-bounded model checker based on the satisfiability modulo theories (SMT) to check for data race, deadlock, pointer safety, array bounds, arithmetic overflow, division by zero, and user-specified assertions in programs written in Compute Unified Device Architecture (CUDA).