Trabalho em anais de evento
BMCLua: Verification of Lua programs in digital TV interactive applications
JANUARIO, FRANCISCO A. P.; CORDEIRO, LUCAS C.; LUCENA, VICENTE F. DE; LIMA FILHO, EDDIE B. DE
Resumo
Resumo
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.
Autoria
Autores do grupo (2)
A lista completa de autores está no topo da página. Abaixo, apenas os pesquisadores do e-Controls vinculados a esta publicação.
palavras-chave
Palavras-chave
bounded model checkingprogram verificationESBMCarray bounds checkingdivision by zerosafety propertiessoftware defect detection
Status
Published
links
Links e arquivos
Trabalho em anais de evento