BMCLua: Verification of Lua Programs in Digital TV Interactive Applications

Francisco A. P. Januario, Lucas C. Cordeiro, Vicente F., Jr. de Lucena, Eddie B. de Lima Filho

Research output: Other contributionpeer-review


The present paper describes a novel scheme for checking for potential defects in Lua programs, by using Bounded Model Checking (BMC). Such an approach, called BMCLua, translates a Lua program into an ANSI-C one, which is then verified by the Efficient SMT-Based Bounded Model Checker (ESBMC). BMCLua is able to check for safety properties related to array bounds, division by zero, and user-specified assertions, in Lua programs. This paper marks the first application of BMC to Lua programs. The experimental results show that the performance of BMCLua is similar to that of ESBMC, in about 70% of the benchmarks used for evaluation.
Original languageEnglish
Number of pages2
Publication statusPublished - 2014


  • Digital TV
  • Model Checking


Dive into the research topics of 'BMCLua: Verification of Lua Programs in Digital TV Interactive Applications'. Together they form a unique fingerprint.

Cite this