@MASTERSTHESIS{ 2019:935492850,
 	title = {Verifica??o limitada de modelos baseada em SMT para programas CUDA},
 	year = {2019},
 	url = "https://tede.ufam.edu.br/handle/tede/7019",
 	abstract = "A ferramenta de verifica??o ESBMC-GPU ? uma extens?o do Verificador de Modelos de Contexto Limitado baseado em SMT (ESBMC), que tem como prop?sito verificar programas de Unidades de Processamento Gr?fico (GPU) escritos na plataforma de Computa??o Unificada da Arquitetura de Dispositivos (CUDA). ESBMC-GPU usa um modelo operacional, i.e., uma abstra??o das bibliotecas do CUDA, que conservativamente aproxima suas sem?nticas para verificar os programas. Assim, s?o exploradas as poss?veis intercala??es (sob um dado limite de contexto), enquanto trata cada uma simbolicamente. Al?m disso, a ferramenta implementa um algoritmo de redu??o monot?nica de ordem parcial para realizar uma an?lise sobre duas threads a fim de reduzir a explora??o do espa?o de estados. Resultados experimentais mostram que o ESBMC-GPU pode, com sucesso, verificar 82% dos benchmarks enquanto mant?m baixas taxas de falsos resultados. A ferramenta tamb?m ? capaz de detectar mais viola??es de propriedades quando comparada a outras ferramentas de verifica??o existentes. Isso ? devido a sua capacidade de verificar erros no fluxo de execu??o do programa e detectar viola??es de condi??es de corrida e acessos fora dos limites de vetores.",
 	publisher = {Universidade Federal do Amazonas},
 	scholl = {Programa de P?s-gradua??o em Engenharia El?trica},
 	note = {Faculdade de Tecnologia}
}