A CONTEXT-BOUNDED MODEL CHECKING TOOL FOR
CUDA PROGRAMS
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).
A visual abstract of ESBMC-GPU can be found here
Data Race
Checks for data race conditions to avoid that multiple threads perform unsynchronized accesses to the shared variable.
Pointer safety
Ensures that (i) the pointer offset does not exceed the object bounds (ii) the pointer is neither NULL nor an invalid object.
Array Bounds
Ensures that the value of the array index is within the known (and fixed) bounds.
Overflow
Checks whether a sum or product exceeds the number representation.
Division by Zero
Checks for a division by zero in arithmetic expressions.
User-specified assertions
Checks for user-specified assertions.
About US
A Model Checker for Compute Unified Device Architecture (CUDA)
ESBMC-GPU http://www.esbmc.org
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).
ESBMC - Efficient SMT-Based Context-Bounded Model Checker
ESBMC is a context-bounded model checker for embedded C/C++ software based on Satisfiability Modulo Theories (SMT) solver. It allows the verification engineer to verify single- and multi-threaded software (with shared variables and locks); to reason about arithmetic under- and overflow, pointer safety, memory leaks, array bounds, atomicity and order violations, deadlock and data race; to verify programs that make use of bit-level, pointers, structs, unions and fixed-point arithmetic.
CONTRIBUTORS
• Celso Carvalho • Eddie B. de Lima Filho • Erickson Alves • Felipe R. Monteiro • Hendrio Marques • Higo Albuquerque • github Ismail • Isabela Silva • Lucas Cordeiro • Phillipe Pereira • Vanessa Santos