BMCLua: Verification of Lua programs in digital TV interactive applications

Author

Januario, F.A.P. ; Cordeiro, L.C. ; De Lucena, V.F. ; De Lima Filho, E.B.

Author_Institution

Fed. Univ. of Amazonas-UFAM, Manaus, Brazil

fYear

2014

fDate

7-10 Oct. 2014

Firstpage

707

Lastpage

708

Abstract

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.

Keywords

authoring languages; computability; digital television; program verification; ANSI-C; BMCLua; ESBMC; Lua program verification; SMT-based bounded model checker; array bounds; bounded model checking; digital TV interactive applications; division by zero; safety properties; satisfiability modulo theories; user-specified assertions; Arrays; Benchmark testing; Computer languages; Digital TV; Model checking; Programming; Syntactics; Digital TV; Lua; Model Checking;

fLanguage

English

Publisher

ieee

Conference_Titel

Consumer Electronics (GCCE), 2014 IEEE 3rd Global Conference on

Conference_Location

Tokyo

Type

conf

DOI

10.1109/GCCE.2014.7031344

Filename

7031344