{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T18:41:34Z","timestamp":1791484894074,"version":"4.3.4"},"publisher-location":"New York, NY, USA","reference-count":23,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,7,10]],"date-time":"2019-07-10T00:00:00Z","timestamp":1562716800000},"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":[],"published-print":{"date-parts":[[2019,7,10]]},"DOI":"10.1145\/3293882.3338999","type":"proceedings-article","created":{"date-parts":[[2019,7,11]],"date-time":"2019-07-11T12:13:31Z","timestamp":1562847211000},"page":"386-389","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["SAFEVM: a safety verifier for Ethereum smart contracts"],"prefix":"10.1145","author":[{"given":"Elvira","family":"Albert","sequence":"first","affiliation":[{"name":"Complutense University of Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jes\u00fas","family":"Correas","sequence":"additional","affiliation":[{"name":"Complutense University of Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pablo","family":"Gordillo","sequence":"additional","affiliation":[{"name":"Complutense University of Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guillermo","family":"Rom\u00e1n-D\u00edez","sequence":"additional","affiliation":[{"name":"Universidad Polit\u00e9cnica de Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Albert","family":"Rubio","sequence":"additional","affiliation":[{"name":"Complutense University of Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,7,10]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2018. Mythril.\n   Available at https:\/\/github.com\/b-mueller\/mythril. \n  2018\n  . \n  Oyente\n  : \n  An Analysis Tool for Smart Contracts\n  . https:\/\/github.com\/ melonproject\/oyente.  2018. Mythril. Available at https:\/\/github.com\/b-mueller\/mythril. 2018. Oyente: An Analysis Tool for Smart Contracts. https:\/\/github.com\/ melonproject\/oyente."},{"key":"e_1_3_2_1_2_1","volume-title":"EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. In ATVA (LNCS)","volume":"11138","author":"Albert E."},{"key":"e_1_3_2_1_3_1","unstructured":"Springer 513\u2013520.  Springer 513\u2013520."},{"key":"e_1_3_2_1_4_1","volume-title":"GASTAP: A Gas Analyzer for Smart Contracts. CoRR abs\/1811.10403","author":"Albert E.","year":"2018"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167084"},{"key":"e_1_3_2_1_6_1","volume-title":"CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. 184\u2013190","author":"Beyer D."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993611"},{"key":"e_1_3_2_1_8_1","volume-title":"Vandal: A Scalable Security Analysis Framework for Smart Contracts. arXiv:1809.03981.","author":"Brent L.","year":"2018"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"M. Brockschmidt D. Larraz A. Oliveras E. Rodr\u00edguez-Carbonell and A. Rubio. 2015. Compositional Safety Verification with Max-SMT. In FMCAD. 33\u201340.   M. Brockschmidt D. Larraz A. Oliveras E. Rodr\u00edguez-Carbonell and A. Rubio. 2015. Compositional Safety Verification with Max-SMT. In FMCAD. 33\u201340.","DOI":"10.1109\/FMCAD.2015.7542250"},{"key":"e_1_3_2_1_10_1","volume-title":"IEEE 24th International Conference on Software Analysis, Evolution and Reengineering, SANER. IEEE Computer Society, 442\u2013446","author":"Chen T."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276486"},{"key":"e_1_3_2_1_12_1","volume-title":"POST (LNCS)","volume":"10804","author":"Grishchenko I."},{"key":"e_1_3_2_1_13_1","unstructured":"Springer 243\u2013269.  Springer 243\u2013269."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158136"},{"key":"e_1_3_2_1_15_1","unstructured":"T. Kahsai J. A. Navas A. Gurfinkel and A. Komuravelli. 2015. The SeaHorn Verification Framework. In CAV.  T. Kahsai J. A. Navas A. Gurfinkel and A. Komuravelli. 2015. The SeaHorn Verification Framework. In CAV."},{"key":"e_1_3_2_1_16_1","volume-title":"ZEUS: Analyzing Safety of Smart Contracts","author":"Kalra S.","year":"2018"},{"key":"e_1_3_2_1_17_1","unstructured":"A. Kolluri I. Nikolic I. Sergey A. Hobor and P. Saxena. 2018. Exploiting The Laws of Order in Smart Contracts. CoRR abs\/1810.11605 (2018). arXiv: 1810.11605  A. Kolluri I. Nikolic I. Sergey A. Hobor and P. Saxena. 2018. Exploiting The Laws of Order in Smart Contracts. CoRR abs\/1810.11605 (2018). arXiv: 1810.11605"},{"key":"e_1_3_2_1_18_1","volume-title":"USENIX Security Symposium. USENIX Association, 1317\u20131333","author":"Krupp J."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_1_20_1","volume-title":"Computing Exact Worst-Case Gas Consumption for Smart Contracts. In ISoLA (LNCS)","volume":"11247","author":"Marescotti M."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274743"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243780"},{"key":"e_1_3_2_1_23_1","unstructured":"G. Wood. 2014. Ethereum: A secure decentralised generalised transaction ledger. Abstract 1 Overview of SAFEVM 2 Translation to C with SV-COMP Annotations 3 Experimental Evaluation 4 Conclusions References  G. Wood. 2014. Ethereum: A secure decentralised generalised transaction ledger. Abstract 1 Overview of SAFEVM 2 Translation to C with SV-COMP Annotations 3 Experimental Evaluation 4 Conclusions References"}],"event":{"name":"ISSTA '19: 28th ACM SIGSOFT International Symposium on Software Testing and Analysis","location":"Beijing China","acronym":"ISSTA '19","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293882.3338999","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3293882.3338999","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:51Z","timestamp":1750207431000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293882.3338999"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,10]]},"references-count":23,"alternative-id":["10.1145\/3293882.3338999","10.1145\/3293882"],"URL":"https:\/\/doi.org\/10.1145\/3293882.3338999","relation":{},"subject":[],"published":{"date-parts":[[2019,7,10]]},"assertion":[{"value":"2019-07-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}