BMCLua: Metodologia para Verificação de Códigos Lua utilizando Bounded Model Checking

Abstract

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.