Paper Info
Title
BMCLua: Verification of Lua programs in digital TV interactive applications
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.
Year
DOI
Venue
2014
10.1109/GCCE.2014.7031344
GCCE
Keywords
Field
DocType
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,digital tv,lua,model checking,programming,computer languages,benchmark testing
Division by zero,Programming language,Model checking,Computer science,Digital television,Benchmark (computing),Bounded function
Conference
Citations 
PageRank 
References 
1
0.36
2
Authors
4
Name
Order
Citations
PageRank
Januario, F.A.P.110.36
Cordeiro, L.C.210.36
de Lucena, V.F.3182.89
E. B. de Lima Filho44512.51