Trabalho em anais de eventoOpen Access
Verificação de Kernels em Programas CUDA usando Bounded Model Checking
Pereira, P. A.; ALBUQUERQUE, H.; MARQUES, H.; SILVA, I.; SANTOS, V.; Carvalho, C. B.; FERREIRA, R. S.; CORDEIRO, L. C
Resumo
Resumo
Este artigo apresenta uma extensão da ferramenta Efficient SMTBased Context-Bounded Model Checker (ESBMC) para verificar programas que executam em unidades de processamento gráfico (GPU), chamado de ESBMCGPU. Em especial, ESBMC-GPU é um verificador de modelos limitado baseado nas teorias do módulo da satisfatibilidade para programas desenvolvidos na arquitetura de dispositivo unificado 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 verificar mais programas CUDA reais do que outras abordagens existentes.
palavras-chave
Palavras-chave
CUDA kernelsbounded model checkingESBMCSMT-based model checkingabstract semantics
Status
Published
links
Links e arquivos
Trabalho em anais de evento