Verificação de Kernels em Programas CUDA usando Bounded Model Checking - Pereira, Phillipe; Albuquerque, Higo; Marques, Hendrio; Silva, Isabela; Santos, Vanessa; Ferreira, Ricardo; Carvalho, Celso; Cordeiro, Lucas (Anais do Simpósio em Sistemas Computacionais de Alto Desempenho (SSCAD), 2015)
Este artigo apresenta uma extensão da ferramenta Efﬁcient SMTBased Context-Bounded Model Checker (ESBMC) para veriﬁcar programas que executam em unidades de processamento gráﬁco (GPU), chamado de ESBMCGPU. Em especial, ESBMC-GPU é um veriﬁcador de modelos limitado baseado nas teorias do módulo da satisfatibilidade para programas desenvolvidos na arquitetura de dispositivo uniﬁcado 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 veriﬁcar mais programas CUDA reais do que outras abordagens existentes.