BMCLua: A Translator for Model Checking Lua Programs

• Published in: Software engineering notes 2017-09, Vol.42 (3), p.1-10
• Main Authors: Monteiro, Felipe R., Januário, Francisco A.P., Cordeiro, Lucas C., de Lima Filho, Eddie B.
• Format: Article
• Language: English
• ISSN: 0163-5948
• DOI: 10.1145/3127360.3127367

Lua is a programming language designed as scripting language, which is fast, lightweight, and suitable for embedded applications. Due to its features, Lua is widely used in the development of games and interactive applications for digital TV. However, during the development phase of such applications, some errors may be introduced, such as deadlock, arithmetic overflow, and division by zero. This paper describes a novel verification approach for software written in Lua, using as backend the Efficient SMTBased Context-Bounded Model Checker (ESBMC). Such an approach, called bounded model checking - Lua (BMCLua), consists in translating Lua programs into ANSI-C source code, which is then verified with ESBMC. Experimental results show that the proposed verification methodology is effective and efficient, when verifying safety properties in Lua programs. The performed experiments have shown that BMCLua produces an ANSI-C code that is more efficient for verification, when compared with other existing approaches. To the best of our knowledge, this work is the first that applies bounded model checking to the verification of Lua programs.