Trabalho em anais de evento
Verifying CUDA programs using SMT-based context-bounded model checking
PEREIRA, PHILLIPE; ALBUQUERQUE, HIGO; MARQUES, HENDRIO; SILVA, ISABELA; CARVALHO, CELSO; Cordeiro, Lucas; SANTOS, VANESSA; FERREIRA, RICARDO
Resumo
Resumo
We present ESBMC-GPU, an extension to the ESBMC model checker that is aimed at verifying GPU programs written for the CUDA framework. ESBMC-GPU uses an operational model for the verification, i.e., an abstract representation of the standard CUDA libraries that conservatively approximates their semantics. ESBMC-GPU verifies CUDA programs, by explicitly exploring the possible interleavings (up to the given context bound), while treating each interleaving itself symbolically. Experimental results show that ESBMC-GPU is able to detect more properties violations, while keeping lower rates of false results.
Autoria
Autores do grupo (1)
A lista completa de autores está no topo da página. Abaixo, apenas os pesquisadores do e-Controls vinculados a esta publicação.
palavras-chave
Palavras-chave
CUDASMT solversoperational semanticssymbolic executioninterleavingfalse positives
Status
Published
links
Links e arquivos
Trabalho em anais de evento