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

ESBMC-GPU is developed at the Federal University of Amazonas (UFAM). This project is funded by the Technological Development Institute (INdT).


A Model Checker for Compute Unified Device Architecture (CUDA)

ESBMC-GPU
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.

http://www.esbmc.org

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