This home page presents a tool under development, called BMCLua, which is a Bounded Model Checker for the Lua programming language.

The goal of the BMCLua tool is to extend the features of ESBMC, which is a context-bounded model checker for embedded C/C++ software, for the Lua programming language. The ESBMC tool implements Bounded Model Checking (BMC) and k-induction techniques based on Satisfiability Modulo Theories (SMT) solvers.

BMCLua runs in the Linux operating system, requiring the installation of the ESBMC tool and a Lua interpreter. As BMCLua is developed in Java, it is also needed to install the JRE for Linux.

The current BMCLua version checks only a subset of the Lua programming language instructions. Future version, which is under development, will check all commands, operators, and structures of the Lua programming language.

All suggestions can be sent for the e-mail bmclua.ufam@gmail.com