{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,17]],"date-time":"2026-04-17T23:43:58Z","timestamp":1776469438934,"version":"3.51.2"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,30]],"date-time":"2020-10-30T00:00:00Z","timestamp":1604016000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Austrian Research Promotion Agency","award":["13808694, COMET K1 SBA"],"award-info":[{"award-number":["13808694, COMET K1 SBA"]}]},{"name":"Internet Foundation Austria","award":["2158"],"award-info":[{"award-number":["2158"]}]},{"name":"Vienna Business Agency","award":["Vienna Cybersecurity and Privacy Research Center"],"award-info":[{"award-number":["Vienna Cybersecurity and Privacy Research Center"]}]},{"name":"European Research Council","award":["771527-BROWSEC"],"award-info":[{"award-number":["771527-BROWSEC"]}]},{"name":"Austrian Science Fund","award":["P31621, W1255-N23"],"award-info":[{"award-number":["P31621, W1255-N23"]}]},{"name":"Google Cloud"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,10,30]]},"DOI":"10.1145\/3372297.3417250","type":"proceedings-article","created":{"date-parts":[[2020,11,2]],"date-time":"2020-11-02T18:27:04Z","timestamp":1604341624000},"page":"621-640","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":102,"title":["eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts"],"prefix":"10.1145","author":[{"given":"Clara","family":"Schneidewind","sequence":"first","affiliation":[{"name":"TU Wien, Vienna, Austria"}]},{"given":"Ilya","family":"Grishchenko","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}]},{"given":"Markus","family":"Scherer","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}]},{"given":"Matteo","family":"Maffei","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}]}],"member":"320","published-online":{"date-parts":[[2020,11,2]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"2016. The DAO Smart Contract.Available at http:\/\/etherscan.io\/address\/0xbb9bc244d798123fde783fcc1c72d3bb8c189413#code.  2016. The DAO Smart Contract.Available at http:\/\/etherscan.io\/address\/0xbb9bc244d798123fde783fcc1c72d3bb8c189413#code."},{"key":"e_1_3_2_2_2_1","unstructured":"2017. The Parity Wallet Breach 30 million ether reported stolen. Available at https:\/\/www.coindesk.com\/30-million-ether-reported-stolen-parity-wallet-breach\/.  2017. The Parity Wallet Breach 30 million ether reported stolen. Available at https:\/\/www.coindesk.com\/30-million-ether-reported-stolen-parity-wallet-breach\/."},{"key":"e_1_3_2_2_3_1","unstructured":"2017. The Parity Wallet Vulnerability. Available at https:\/\/paritytech.io\/blog\/security-alert.html.  2017. The Parity Wallet Vulnerability. Available at https:\/\/paritytech.io\/blog\/security-alert.html."},{"key":"e_1_3_2_2_4_1","unstructured":"2019. SafeMath library source. https:\/\/github.com\/OpenZeppelin\/openzeppelin-contracts\/blob\/master\/contracts\/math\/SafeMath.sol.  2019. SafeMath library source. https:\/\/github.com\/OpenZeppelin\/openzeppelin-contracts\/blob\/master\/contracts\/math\/SafeMath.sol."},{"key":"e_1_3_2_2_5_1","unstructured":"2019. Solidity. https:\/\/solidity.readthedocs.io\/.  2019. Solidity. https:\/\/solidity.readthedocs.io\/."},{"key":"e_1_3_2_2_6_1","unstructured":"2020. eThor: extended version source code build and evaluation artifacts. https:\/\/secpriv.wien\/ethor.  2020. eThor: extended version source code build and evaluation artifacts. https:\/\/secpriv.wien\/ethor."},{"key":"e_1_3_2_2_7_1","unstructured":"2020. SMT-LIB. Available at http:\/\/smtlib.cs.uiowa.edu\/language.shtml.  2020. SMT-LIB. Available at http:\/\/smtlib.cs.uiowa.edu\/language.shtml."},{"key":"e_1_3_2_2_8_1","unstructured":"Chandra Adhikari. 2017. Secure Framework for Healthcare Data Management Using Ethereum-based Blockchain Technology. (2017).  Chandra Adhikari. 2017. Secure Framework for Healthcare Data Management Using Ethereum-based Blockchain Technology. (2017)."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Sidney Amani Myriam B\u00e9gel Maksym Bortin and Mark Staples. 2018. Towards Verifying Ethereum Smart Contract Bytecode in Isabelle\/HOL.CPP. ACM. Toappear(2018).  Sidney Amani Myriam B\u00e9gel Maksym Bortin and Mark Staples. 2018. Towards Verifying Ethereum Smart Contract Bytecode in Isabelle\/HOL.CPP. ACM. Toappear(2018).","DOI":"10.1145\/3176245.3167084"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54455-6_8"},{"key":"e_1_3_2_2_11_1","volume-title":"International Conference on. IEEE, 25--30","author":"Azaria Asaph","year":"2016","unstructured":"Asaph Azaria , Ariel Ekblaw , Thiago Vieira , and Andrew Lippman . 2016 . Medrec:Using Blockchain for Medical Data Access and Permission Management. In Open and Big Data (OBD) , International Conference on. IEEE, 25--30 . Asaph Azaria, Ariel Ekblaw, Thiago Vieira, and Andrew Lippman. 2016. Medrec:Using Blockchain for Medical Data Access and Permission Management. In Open and Big Data (OBD), International Conference on. IEEE, 25--30."},{"key":"e_1_3_2_2_12_1","volume-title":"Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security. ACM, 91--96","author":"Bhargavan Karthikeyan","unstructured":"Karthikeyan Bhargavan , Antoine Delignat-Lavaud , C\u00e9dric Fournet , Anitha Gollamudi , Georges Gonthier , Nadim Kobeissi , Natalia Kulatova , Aseem Rastogi , Thomas Sibut-Pinote , Nikhil Swamy , Formal verification of smart contracts: Short paper . In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security. ACM, 91--96 . Karthikeyan Bhargavan, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi,Thomas Sibut-Pinote, Nikhil Swamy, et al.2016. Formal verification of smart contracts: Short paper. In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security. ACM, 91--96."},{"key":"e_1_3_2_2_13_1","volume-title":"Findel: Secure Derivative Contracts for Ethereum. In International Conference on Financial Cryptography and Data Security. Springer, 453--467","author":"Biryukov Alex","year":"2017","unstructured":"Alex Biryukov , Dmitry Khovratovich , and Sergei Tikhomirov . 2017 . Findel: Secure Derivative Contracts for Ethereum. In International Conference on Financial Cryptography and Data Security. Springer, 453--467 . Alex Biryukov, Dmitry Khovratovich, and Sergei Tikhomirov. 2017. Findel: Secure Derivative Contracts for Ethereum. In International Conference on Financial Cryptography and Data Security. Springer, 453--467."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"crossref","unstructured":"Nikolaj Bj\u00f8rner Arie Gurfinkel Ken McMillan and Andrey Rybalchenko. 2015.Horn clause solvers for program verification. In Fields of Logic and Computation II. Springer 24--51.  Nikolaj Bj\u00f8rner Arie Gurfinkel Ken McMillan and Andrey Rybalchenko. 2015.Horn clause solvers for program verification. In Fields of Logic and Computation II. Springer 24--51.","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321996"},{"key":"e_1_3_2_2_16_1","volume-title":"Building the Information Society","author":"Cousot Patrick","unstructured":"Patrick Cousot and Radhia Cousot . 2004. Basic concepts of abstract interpretation . In Building the Information Society . Springer , 359--366. Patrick Cousot and Radhia Cousot. 2004. Basic concepts of abstract interpretation. In Building the Information Society. Springer, 359--366."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/DAPPCON.2019.00018"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"crossref","unstructured":"Changyu Dong Yilei Wang Amjad Aldweesh Patrick McCorry and Aad van Moorsel. 2017. Betrayal Distrust and Rationality: Smart Counter-Collusion Contracts for Verifiable Cloud Computing. (2017).  Changyu Dong Yilei Wang Amjad Aldweesh Patrick McCorry and Aad van Moorsel. 2017. Betrayal Distrust and Rationality: Smart Counter-Collusion Contracts for Verifiable Cloud Computing. (2017).","DOI":"10.1145\/3133956.3134032"},{"key":"e_1_3_2_2_19_1","unstructured":"Ethereum 2018. Solidity Docs. Ethereum. https:\/\/solidity.readthedocs.io\/en\/develop\/control-structures.html#error-handling-assert-require-revert-and-exceptions  Ethereum 2018. Solidity Docs. Ethereum. https:\/\/solidity.readthedocs.io\/en\/develop\/control-structures.html#error-handling-assert-require-revert-and-exceptions"},{"key":"e_1_3_2_2_20_1","unstructured":"Ethereum 2019. Solidity Docs. Ethereum. https:\/\/solidity.readthedocs.io\/en\/v0.5.13\/security-considerations  Ethereum 2019. Solidity Docs. Ethereum. https:\/\/solidity.readthedocs.io\/en\/v0.5.13\/security-considerations"},{"key":"e_1_3_2_2_21_1","volume-title":"Systems, Languages & Applications OOPSLA","author":"Grech Neville","year":"2018","unstructured":"Neville Grech , Michael Kong , Anton Jurisevic , Lexi Brent , Bernhard Scholz , and Yannis Smaragdakis . 2018. MadMax: Surviving Out-of-gas Conditions in Ethereum Smart Contracts. Object-Oriented Programming , Systems, Languages & Applications OOPSLA ( 2018 ). Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis. 2018. MadMax: Surviving Out-of-gas Conditions in Ethereum Smart Contracts. Object-Oriented Programming, Systems, Languages & Applications OOPSLA (2018)."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_4"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89722-6_10"},{"key":"e_1_3_2_2_24_1","volume-title":"Proceedings of the ACMon Programming Languages 2, POPL","author":"Grossman Shelly","year":"2017","unstructured":"Shelly Grossman , Ittai Abraham , Guy Golan-Gueta , Yan Michalevsky , Noam Rinetzky , Mooly Sagiv , and Yoni Zohar . 2017 . Online detection of effectively callback free objects with applications to smart contracts . Proceedings of the ACMon Programming Languages 2, POPL (2017), 48. Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar. 2017. Online detection of effectively callback free objects with applications to smart contracts. Proceedings of the ACMon Programming Languages 2, POPL (2017), 48."},{"key":"e_1_3_2_2_25_1","volume-title":"Smart Contract-Based Campus Demonstration of Decentralized Transactive Energy Auctions. In Power & Energy Society Innovative Smart Grid Technologies Conference(ISGT)","author":"Hahn Adam","year":"2017","unstructured":"Adam Hahn , Rajveer Singh , Chen-Ching Liu , and Sijie Chen . 2017 . Smart Contract-Based Campus Demonstration of Decentralized Transactive Energy Auctions. In Power & Energy Society Innovative Smart Grid Technologies Conference(ISGT) , 2017 IEEE. IEEE, 1--5. Adam Hahn, Rajveer Singh, Chen-Ching Liu, and Sijie Chen. 2017. Smart Contract-Based Campus Demonstration of Decentralized Transactive Energy Auctions. In Power & Energy Society Innovative Smart Grid Technologies Conference(ISGT), 2017 IEEE. IEEE, 1--5."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000457"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"crossref","unstructured":"Everett Hildenbrandt Manasvi Saxena Xiaoran Zhu Nishant Rodrigues Philip Daian Dwight Guth and Grigore Rosu. 2017.KEVM: A Complete Semantics of the Ethereum Virtual Machine. Technical Report.  Everett Hildenbrandt Manasvi Saxena Xiaoran Zhu Nishant Rodrigues Philip Daian Dwight Guth and Grigore Rosu. 2017.KEVM: A Complete Semantics of the Ethereum Virtual Machine. Technical Report.","DOI":"10.1109\/CSF.2018.00022"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70278-0_33"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_36"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_23"},{"key":"e_1_3_2_2_32_1","volume-title":"ZEUS: Analyzing Safety of Smart Contracts. NDSS.","author":"Kalra Sukrit","year":"2018","unstructured":"Sukrit Kalra , Seep Goel , Mohan Dhawan , and Subodh Sharma . 2018 . ZEUS: Analyzing Safety of Smart Contracts. NDSS. Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. 2018. ZEUS: Analyzing Safety of Smart Contracts. NDSS."},{"key":"e_1_3_2_2_33_1","volume-title":"Proceedings of the 27th USENIX Conference on Security Symposium (SEC'18)","author":"Krupp Johannes","year":"2018","unstructured":"Johannes Krupp and Christian Rossow . 2018 . TEETHER: Gnawing at Ethereum to Automatically Exploit Smart Contracts . In Proceedings of the 27th USENIX Conference on Security Symposium (SEC'18) . USENIX Association, 1317--1333. Johannes Krupp and Christian Rossow. 2018. TEETHER: Gnawing at Ethereum to Automatically Exploit Smart Contracts. In Proceedings of the 27th USENIX Conference on Security Symposium (SEC'18). USENIX Association, 1317--1333."},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2921624"},{"key":"e_1_3_2_2_35_1","unstructured":"Ning Lu Bin Wang Yongxin Zhang Wenbo Shi and Christian Esposito. 2019. NeuCheck: A more practical Ethereum smart contract security analysis tool.Software: Practice and Experience(2019).  Ning Lu Bin Wang Yongxin Zhang Wenbo Shi and Christian Esposito. 2019. NeuCheck: A more practical Ethereum smart contract security analysis tool.Software: Practice and Experience(2019)."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_2_37_1","volume-title":"Blocktix: Decentralized Event Hosting and Ticket Distribution Network.","author":"Mathieu Florian","year":"2017","unstructured":"Florian Mathieu and Ryno Mathee . 2017 . Blocktix: Decentralized Event Hosting and Ticket Distribution Network. (2017). Available at https:\/\/blocktix.io\/public\/doc\/blocktix-wp-draft.pdf . Florian Mathieu and Ryno Mathee. 2017. Blocktix: Decentralized Event Hosting and Ticket Distribution Network. (2017). Available at https:\/\/blocktix.io\/public\/doc\/blocktix-wp-draft.pdf ."},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70972-7_20"},{"key":"e_1_3_2_2_39_1","volume-title":"Bitcoin: A Peer-to-Peer Electronic Cash System.","author":"Nakamoto Satoshi","year":"2008","unstructured":"Satoshi Nakamoto . 2008 . Bitcoin: A Peer-to-Peer Electronic Cash System. Available at http:\/\/bitcoin.org\/bitcoin.pdf. Satoshi Nakamoto. 2008. Bitcoin: A Peer-to-Peer Electronic Cash System. Available at http:\/\/bitcoin.org\/bitcoin.pdf."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"crossref","unstructured":"Ivica Nikolic Aashish Kolluri Ilya Sergey Prateek Saxena and Aquinas Hobor. 2018. Finding The Greedy Prodigal and Suicidal Contracts at Scale. arXiv preprint arXiv:1802.06038(2018).  Ivica Nikolic Aashish Kolluri Ilya Sergey Prateek Saxena and Aquinas Hobor. 2018. Finding The Greedy Prodigal and Suicidal Contracts at Scale. arXiv preprint arXiv:1802.06038(2018).","DOI":"10.1145\/3274694.3274743"},{"key":"e_1_3_2_2_41_1","volume-title":"Trading Stocks on Blocks-Engineering Decentralized Markets. In International Conference on Design Science Research in Information Systems. Springer, 474--478","author":"Notheisen Benedikt","year":"2017","unstructured":"Benedikt Notheisen , Magnus G\u00f6dde , and Christof Weinhardt . 2017 . Trading Stocks on Blocks-Engineering Decentralized Markets. In International Conference on Design Science Research in Information Systems. Springer, 474--478 . Benedikt Notheisen, Magnus G\u00f6dde, and Christof Weinhardt. 2017. Trading Stocks on Blocks-Engineering Decentralized Markets. In International Conference on Design Science Research in Information Systems. Springer, 474--478."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3264591"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61467-6_14"},{"key":"e_1_3_2_2_44_1","volume-title":"Proc. of 2nd ILPC(1984)","author":"Tamaki Hisao","year":"1984","unstructured":"Hisao Tamaki . 1984 . Unfold\/fold transformation of logic programs . Proc. of 2nd ILPC(1984) , 127--138. Hisao Tamaki. 1984. Unfold\/fold transformation of logic programs. Proc. of 2nd ILPC(1984), 127--138."},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274737"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243780"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2905428"},{"key":"e_1_3_2_2_48_1","volume-title":"Mobility and Security (NTMS), 2018 9th IFIP International Conference on. IEEE, 1--5.","author":"Zhou Ence","year":"2018","unstructured":"Ence Zhou , Song Hua , Bingfeng Pi , Jun Sun , Yashihide Nomura , Kazuhiro Yamashita , and Hidetoshi Kurihara . 2018 . Security Assurance for Smart Contract. In New Technologies , Mobility and Security (NTMS), 2018 9th IFIP International Conference on. IEEE, 1--5. Ence Zhou, Song Hua, Bingfeng Pi, Jun Sun, Yashihide Nomura, Kazuhiro Yamashita, and Hidetoshi Kurihara. 2018. Security Assurance for Smart Contract. In New Technologies, Mobility and Security (NTMS), 2018 9th IFIP International Conference on. IEEE, 1--5."}],"event":{"name":"CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security","location":"Virtual Event USA","acronym":"CCS '20","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372297.3417250","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372297.3417250","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:01:30Z","timestamp":1750197690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372297.3417250"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,30]]},"references-count":48,"alternative-id":["10.1145\/3372297.3417250","10.1145\/3372297"],"URL":"https:\/\/doi.org\/10.1145\/3372297.3417250","relation":{},"subject":[],"published":{"date-parts":[[2020,10,30]]},"assertion":[{"value":"2020-11-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}