Submitted by Kamila Costa (kamilavasconceloscosta@gmail.com) on 2015-08-03T12:38:15Z No. of bitstreams: 2 Dissertação - Francisco de A P Januário.pdf: 1215702 bytes, checksum: 7f02a7976f19b94633a48b22a4990adf (MD5) ficha_catalografica.pdf: 1919 bytes, checksum: cbf0df9103c43df7202f18e8010435b9 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-08-04T15:34:24Z (GMT) No. of bitstreams: 2 Dissertação - Francisco de A P Januário.pdf: 1215702 bytes, checksum: 7f02a7976f19b94633a48b22a4990adf (MD5) ficha_catalografica.pdf: 1919 bytes, checksum: cbf0df9103c43df7202f18e8010435b9 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-08-04T15:38:25Z (GMT) No. of bitstreams: 2 Dissertação - Francisco de A P Januário.pdf: 1215702 bytes, checksum: 7f02a7976f19b94633a48b22a4990adf (MD5) ficha_catalografica.pdf: 1919 bytes, checksum: cbf0df9103c43df7202f18e8010435b9 (MD5) / Made available in DSpace on 2015-08-04T15:38:25Z (GMT). No. of bitstreams: 2 Dissertação - Francisco de A P Januário.pdf: 1215702 bytes, checksum: 7f02a7976f19b94633a48b22a4990adf (MD5) ficha_catalografica.pdf: 1919 bytes, checksum: cbf0df9103c43df7202f18e8010435b9 (MD5) Previous issue date: 2015-04-01 / CNPq - Conselho Nacional de Desenvolvimento Científico e Tecnológico / The development of programs written in Lua programming language, which is largely used in applications for digital TV and games, can cause errors, deadlocks, arithmetic overflow, and division by zero. This work aims to propose a methodology for checking programs written in Lua programming language using the Efficient SMT-Based Context-BoundedModel Checker (ESBMC) tool, which represents the state-of-the-art context-bounded model checker. It is used for ANSI-C/C++ programs and has the ability to verify array out-of-bounds, division by zero, and user-defined assertions. The proposed approach consists in translating programs written in Lua to an intermediate language, which are further verified by ESBMC. The translator is developed with the ANTLR (ANother Tool for Language Recognition) tool, which is used for developing the lexer and parser, based on the Lua language grammar. This work is motivated by the need for extending the benefits of bounded model checking, based on satisfiability modulotheories, to programs written in Lua programming language. The experimental results show that the proposed methodology can be very effective, regarding model checking (safety) of Luaprogramming language properties. / 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.