@MASTERSTHESIS{ 2015:847922928,
 	title = {BMCLua: Metodologia para Verificação de Códigos Lua utilizando Bounded Model Checking},
 	year = {2015},
 	url = "http://tede.ufam.edu.br/handle/tede/4539",
 	abstract = "O desenvolvimento de programas escritos na linguagem de programação Lua, que é
 muito utilizada em aplicações para TV digital e jogos, pode gerar erros, deadlocks, estouro
 aritmético e divisão por zero. Este trabalho tem como objetivo propor uma metodologia de
 verificação para programas escritos na linguagem de programação Lua usando a ferramenta
 Efficient SMT-Based Context-Bounded Model Checker (ESBMC), que representa o estado da
 arte em verificação de modelos de contexto limitado. O ESBMC é aplicado a programas embarcados
 ANSI-C/C++ e possui a capacidade de verificar estouro de limites de vetores, divisão
 por zero e assertivas definidas pelo usuário. A abordagem proposta consiste na tradução de
 programas escritos em Lua para uma linguagem intermediária, que é posteriormente verificada
 pelo ESBMC. O tradutor foi desenvolvido com a ferramenta ANTLR (do inglês “ANother Tool
 for Language Recognition”), que é utilizada na construção de analisadores léxicos e sintáticos,
 a partir da gramática da linguagem Lua. Este trabalho é motivado pela necessidade de se
 estender os benefícios da verificação de modelos, baseada nas teorias de satisfatibilidade, a programas
 escritos na linguagem de programação Lua. Os resultados experimentais mostram que
 a metodologia proposta pode ser muito eficaz, no que diz respeito à verificação de propriedades
 (segurança) da linguagem de programação Lua.",
 	publisher = {Universidade Federal do Amazonas},
 	scholl = {Programa de Pós-graduação em Engenharia Elétrica},
 	note = {Faculdade de Tecnologia}
}