Verificação de Códigos Lua Utilizando BMCLua

O presente artigo descreve uma abordagem de verificação de possíveis defeitos em códigos Lua, através da ferramenta Bounded Model Checker. Tal abordagem traduz código escrito em Lua para ANSI-C e o avalia através do Efficient SMT-Based Context-Bounded Model Checker (ESBMC), que é um verificador de modelos de contexto limitado para códigos 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. Este trabalho é motivado pela necessidade de se estender os benefícios da verificação de modelos, baseada nas teorias de satisfatibilidade, para códigos escritos na linguagem Lua. Os resultados apresentados, neste artigo, mostram a viabilidade da verificação de códigos Lua através da ferramenta ESBMC.