Verificação de Kernels em Programas CUDA usando Bounded Model Checking

Este artigo apresenta uma extensão da ferramenta Efcient SMTBased Context-Bounded Model Checker (ESBMC) para vericar programas que executam em unidades de processamento gráco (GPU), chamado de ESBMCGPU. Em especial, ESBMC-GPU é um vericador de modelos limitado baseado nas teorias do módulo da satisfatibilidade para programas desenvolvidos na arquitetura de dispositivo unicado de computação (CUDA). O ESBMC-GPU é baseado em um modelo operacional, uma representação abstrata das bibliotecas padrões do CUDA que conservadoramente aproxima suas semânticas. Com ESBMC-GPU, é possível vericar mais programas CUDA reais do que outras abordagens existentes.