{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T04:07:36Z","timestamp":1750910856292,"version":"3.41.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,9,5]],"date-time":"2017-09-05T00:00:00Z","timestamp":1504569600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2017,9,5]]},"abstract":"<jats:p>Lua is a programming language designed as scripting language, which is fast, lightweight, and suitable for embedded applications. Due to its features, Lua is widely used in the development of games and interactive applications for digital TV. However, during the development phase of such applications, some errors may be introduced, such as deadlock, arithmetic overflow, and division by zero. This paper describes a novel verification approach for software written in Lua, using as backend the Efficient SMTBased Context-Bounded Model Checker (ESBMC). Such an approach, called bounded model checking - Lua (BMCLua), consists in translating Lua programs into ANSI-C source code, which is then verified with ESBMC. Experimental results show that the proposed verification methodology is effective and efficient, when verifying safety properties in Lua programs. The performed experiments have shown that BMCLua produces an ANSI-C code that is more efficient for verification, when compared with other existing approaches. To the best of our knowledge, this work is the first that applies bounded model checking to the verification of Lua programs.<\/jats:p>","DOI":"10.1145\/3127360.3127367","type":"journal-article","created":{"date-parts":[[2017,9,7]],"date-time":"2017-09-07T13:02:09Z","timestamp":1504789329000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["BMCLua"],"prefix":"10.1145","volume":"42","author":[{"given":"Felipe R.","family":"Monteiro","sequence":"first","affiliation":[{"name":"Federal University of Amazonas, Manaus, Brazil"}]},{"given":"Francisco A.P.","family":"Janu\u00e1rio","sequence":"additional","affiliation":[{"name":"Federal University of Amazonas, Manaus, Brazil"}]},{"given":"Lucas C.","family":"Cordeiro","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, UK"}]},{"given":"Eddie B.","family":"de Lima Filho","sequence":"additional","affiliation":[{"name":"Samsung Electronics Ltda., Manaus, Brazil"}]}],"member":"320","published-online":{"date-parts":[[2017,9,5]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"ABNT NBR 15606-2: \"Digital Terrestrial Television Data Coding and Transmission Speci cation for Digital Broadcasting Part 2: Ginga-NCL for xed and mobile receivers XML application language for application coding\"; (2009). ABNT NBR 15606-2: \"Digital Terrestrial Television Data Coding and Transmission Speci cation for Digital Broadcasting Part 2: Ginga-NCL for xed and mobile receivers XML application language for application coding\"; (2009)."},{"key":"e_1_2_1_2_1","unstructured":"Aho Alfred V. and Sethi Ravi and Ullman Jeffrey D.: \"Compilers: Principles Techniques and Tools\"; Addison-Wesley Boston \/ MA (1986). Aho Alfred V. and Sethi Ravi and Ullman Jeffrey D.: \"Compilers: Principles Techniques and Tools\"; Addison-Wesley Boston \/ MA (1986)."},{"key":"e_1_2_1_3_1","first-page":"1","article-title":"Bounded model checking of software using SMT solvers instead of SAT solvers","volume":"11","author":"Alessandro Armando","year":"2009","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"e_1_2_1_4_1","unstructured":"Baier C. and Katoen J.: \"Principles of Model Checking (Representation and Mind Series)\"; The MIT Press. (2008). Baier C. and Katoen J.: \"Principles of Model Checking (Representation and Mind Series)\"; The MIT Press. (2008)."},{"key":"e_1_2_1_5_1","unstructured":"Bannister M. J. and Eppstein D.: \"Randomised Speedup of the Bellman-Ford Algorithm\"; CoRR Cornell 1111.5414 (2011); available at: http:\/\/dblp.uni-trier.de\/db\/journals\/corr\/corr1111.html#abs-1111-5414 Bannister M. J. and Eppstein D.: \"Randomised Speedup of the Bellman-Ford Algorithm\"; CoRR Cornell 1111.5414 (2011); available at: http:\/\/dblp.uni-trier.de\/db\/journals\/corr\/corr1111.html#abs-1111-5414"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/SBGAMES.2009.26"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Barnes J.: \"Programming in Ada\"; Cambridge University Press. (2014). Barnes J.: \"Programming in Ada\"; Cambridge University Press. (2014).","DOI":"10.1017\/CBO9781139696616"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"Barrett C. and Stump A. and Tinelli C.: \"The Satisfiability Modulo Theories Library (SMT-LIB)\"; (2010); available at: www.SMT-LIB.org Barrett C. and Stump A. and Tinelli C.: \"The Satisfiability Modulo Theories Library (SMT-LIB)\"; (2010); available at: www.SMT-LIB.org","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_55"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1550723"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205051"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.59"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_42"},{"key":"e_1_2_1_16_1","unstructured":"Cormen T. H. and Stein C. and Rivest R. L. and Leiserson C. E.: \"Introduction to Algorithms\"; McGraw-Hill Higher Education (2001). Cormen T. H. and Stein C. and Rivest R. L. and Leiserson C. E.: \"Introduction to Algorithms\"; McGraw-Hill Higher Education (2001)."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCE.2012.6311359"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"de Melo Brand\u00e3o R. R. and de Souza Filho G. L. and Batista C. E. C. F. and Gomes Soares L. F.: \"Extended features for the Ginga-NCL environment: introducing the LuaTV API\"; Proc. of the 19th International Conference on Computer Communications and Networks IEEE (2010) 1--6. de Melo Brand\u00e3o R. R. and de Souza Filho G. L. and Batista C. E. C. F. and Gomes Soares L. F.: \"Extended features for the Ginga-NCL environment: introducing the LuaTV API\"; Proc. of the 19th International Conference on Computer Communications and Networks IEEE (2010) 1--6.","DOI":"10.1109\/ICCCN.2010.5560066"},{"key":"e_1_2_1_19_1","unstructured":"Deitel H. M. and Deite P. J.: \"Java: How to Program\"; Prentice Hall: Upper Saddle River (2010) 315--336. Deitel H. M. and Deite P. J.: \"Java: How to Program\"; Prentice Hall: Upper Saddle River (2010) 315--336."},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Dirk Beyer M. Erkan Keremoglu.: \"CPAchecker: A Tool for Configurable Software Veri cation\"; CAV (2011) 184--190. Dirk Beyer M. Erkan Keremoglu.: \"CPAchecker: A Tool for Configurable Software Veri cation\"; CAV (2011) 184--190.","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"e_1_2_1_21_1","unstructured":"Fleutot F. and L. Tratt L.: \"Contrasting compile-time meta-programming in Metalua and Converge\"; Proc. of the 3rd Workshop on Dynamic Languages and Applications ACM (2007) 1--10. Fleutot F. and L. Tratt L.: \"Contrasting compile-time meta-programming in Metalua and Converge\"; Proc. of the 3rd Workshop on Dynamic Languages and Applications ACM (2007) 1--10."},{"key":"e_1_2_1_22_1","unstructured":"Friedman D. P. and Wand M.: \"Essentials of Programming Languages 3rd Edition\"; The MIT Press. (2008) 55--65. Friedman D. P. and Wand M.: \"Essentials of Programming Languages 3rd Edition\"; The MIT Press. (2008) 55--65."},{"volume-title":"SPIN 2016; 97--103","author":"Garcia M. P.","key":"e_1_2_1_23_1"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050043"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Havelund K and Skakkeb\u00e6k J U.: \"Applying Model Checking in Java Verification\"; In Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking Dennis Dams Rob Gerth Stefan Leue and Mieke Massink (Eds.). Springer-Verlag London UK (1999) 216--231. Havelund K and Skakkeb\u00e6k J U.: \"Applying Model Checking in Java Verification\"; In Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking Dennis Dams Rob Gerth Stefan Leue and Mieke Massink (Eds.). Springer-Verlag London UK (1999) 216--231.","DOI":"10.1007\/3-540-48234-2_17"},{"key":"e_1_2_1_26_1","unstructured":"Heineman G. and Pollice G. and Selkow S.: \"Algorithms in a Nutshell\"; O'Reilly Media Inc. (2008) 160--164. Heineman G. and Pollice G. and Selkow S.: \"Algorithms in a Nutshell\"; O'Reilly Media Inc. (2008) 160--164."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2007.150"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Janu\u00e1rio F. A. P. and Cordeiro L. C. and de Lucena Jr. V. F. and de Lima Filho E. B.: \"BMCLua: verification of Lua programs in digital TV interactive applications\"; Proc. of the 3rd Global Conference on Consumer Electronics IEEE (2014) 707--708. Janu\u00e1rio F. A. P. and Cordeiro L. C. and de Lucena Jr. V. F. and de Lima Filho E. B.: \"BMCLua: verification of Lua programs in digital TV interactive applications\"; Proc. of the 3rd Global Conference on Consumer Electronics IEEE (2014) 707--708.","DOI":"10.1109\/GCCE.2014.7031344"},{"key":"e_1_2_1_29_1","unstructured":"Janu\u00e1rio F. A. P. Cordeiro L. C. Lima Filho E. B. ; Lucena Jr. V. F.: \"BMCLua: Verifica\u00e7\u00e3o de Programas Lua em Aplica\u00e7\u00f5es Interativas de TV Digital\"; Proc. of the 4th Simp\u00f3sio Brasileiro de Engenharia de Sistemas Computacionais SBESC (2014) 1--6. Janu\u00e1rio F. A. P. Cordeiro L. C. Lima Filho E. B. ; Lucena Jr. V. F.: \"BMCLua: Verifica\u00e7\u00e3o de Programas Lua em Aplica\u00e7\u00f5es Interativas de TV Digital\"; Proc. of the 4th Simp\u00f3sio Brasileiro de Engenharia de Sistemas Computacionais SBESC (2014) 1--6."},{"key":"e_1_2_1_30_1","unstructured":"Jung K. and Brown A.: \"Beginning Lua Programming\"; Wiley (2007) 35--42. Jung K. and Brown A.: \"Beginning Lua Programming\"; Wiley (2007) 35--42."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33542-6_69"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/355588.365140"},{"key":"e_1_2_1_33_1","unstructured":"Lerusalimschy R.: \"Programming in Lua Second Edition\"; Lua.Org (2006). Lerusalimschy R.: \"Programming in Lua Second Edition\"; Lua.Org (2006)."},{"key":"e_1_2_1_34_1","unstructured":"Manura D.: \"Lua To Cee\"; (2012); available at: http:\/\/lua-users.org\/wiki\/LuaToCee Manura D.: \"Lua To Cee\"; (2012); available at: http:\/\/lua-users.org\/wiki\/LuaToCee"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_48"},{"volume-title":"GCCE 2015; 179--447","author":"Monteiro F. R.","key":"e_1_2_1_36_1"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.1632"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_47"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_31"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10452-7_3"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_2_1_43_1","unstructured":"Parr T.: \"The Definitive ANTLR Reference: Building Domain-Specific Languages\"; Pragmatic Bookshelf (2007). Parr T.: \"The Definitive ANTLR Reference: Building Domain-Specific Languages\"; Pragmatic Bookshelf (2007)."},{"key":"e_1_2_1_44_1","first-page":"24","author":"Pereira P","year":"2015","journal-title":"WSCAD-SSC"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2851613.2851830"},{"key":"e_1_2_1_46_1","doi-asserted-by":"crossref","unstructured":"Pereira P. Albuquerque H. Silva I. Marques H. Monteiro F. R. Ferreira R. Cordeiro L. C. SMT-Based Context-Bounded Model Checking for CUDA Programs Concurrency Computat.: Pract. Exper. (2016) Pereira P. Albuquerque H. Silva I. Marques H. Monteiro F. R. Ferreira R. Cordeiro L. C. SMT-Based Context-Bounded Model Checking for CUDA Programs Concurrency Computat.: Pract. Exper. (2016)","DOI":"10.1145\/2851613.2851830"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECBS.2013.15"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/U-MEDIA.2011.59"},{"key":"e_1_2_1_49_1","unstructured":"Schildt H.: \"Java: The Complete Reference (Complete Reference Series)\"; Oracle Press. (2014). Schildt H.: \"Java: The Complete Reference (Complete Reference Series)\"; Oracle Press. (2014)."},{"key":"e_1_2_1_50_1","unstructured":"Sedgewick R.: \"Algorithms in C++ Parts 1-4: Fundamentals Data Structure Sorting Searching Third Edition\"; Addison-Wesley (1998) 273--274. Sedgewick R.: \"Algorithms in C++ Parts 1-4: Fundamentals Data Structure Sorting Searching Third Edition\"; Addison-Wesley (1998) 273--274."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1590\/S0104-65002007000100005"},{"key":"e_1_2_1_52_1","unstructured":"Stroustrup B.: \"The C++ Programming Language - Special Edition\"; Addison Wesley (2007). Stroustrup B.: \"The C++ Programming Language - Special Edition\"; Addison Wesley (2007)."},{"key":"e_1_2_1_53_1","doi-asserted-by":"crossref","unstructured":"Stump A. and Barrett C. W. and Dill D. L.: \"CVC: a cooperating validity checker\"; Proc. of the 14th International Conference on Computer-Aided Verification Springer-Verlag (2002) 500--504. Stump A. and Barrett C. W. and Dill D. L.: \"CVC: a cooperating validity checker\"; Proc. of the 14th International Conference on Computer-Aided Verification Springer-Verlag (2002) 500--504.","DOI":"10.1007\/3-540-45657-0_40"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3127360.3127367","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3127360.3127367","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T16:35:31Z","timestamp":1750869331000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3127360.3127367"}},"subtitle":["A Translator for Model Checking Lua Programs"],"short-title":[],"issued":{"date-parts":[[2017,9,5]]},"references-count":53,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,9,5]]}},"alternative-id":["10.1145\/3127360.3127367"],"URL":"https:\/\/doi.org\/10.1145\/3127360.3127367","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2017,9,5]]},"assertion":[{"value":"2017-09-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}