Trabalho em anais de evento
Verificação de Códigos Lua Utilizando BMCLua
JANUARIO, F. A. P.; CORDEIRO, L. C.; Lima Filho, E. B
Resumo
Resumo
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.
palavras-chave
Palavras-chave
Luacode verificationbenchmarking
Status
Published
links
Links e arquivos
Trabalho em anais de evento