{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:03:22Z","timestamp":1770285802723,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,12,21]],"date-time":"2020-12-21T00:00:00Z","timestamp":1608508800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF-SaTC","award":["1908494"],"award-info":[{"award-number":["1908494"]}]},{"name":"NSF-CCF","award":["1651225"],"award-info":[{"award-number":["1651225"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,12,21]]},"DOI":"10.1145\/3324884.3416646","type":"proceedings-article","created":{"date-parts":[[2021,1,27]],"date-time":"2021-01-27T23:38:56Z","timestamp":1611790736000},"page":"1141-1152","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Summary-based symbolic evaluation for smart contracts"],"prefix":"10.1145","author":[{"given":"Yu","family":"Feng","sequence":"first","affiliation":[{"name":"University of California"}]},{"given":"Emina","family":"Torlak","sequence":"additional","affiliation":[{"name":"University of Washington"}]},{"given":"Rastislav","family":"Bodik","sequence":"additional","affiliation":[{"name":"University of Washington"}]}],"member":"320","published-online":{"date-parts":[[2021,1,27]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"The Coq Proof Assistant. https:\/\/coq.inria.fr\/. [Online","year":"2019","unstructured":"2016. The Coq Proof Assistant. https:\/\/coq.inria.fr\/. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_2_1","volume-title":"GovernMental's 1100 ETH payout is stuck because it uses too much gas. https:\/\/tinyurl.com\/y83dn2yf\/. [Online","year":"2019","unstructured":"2016. GovernMental's 1100 ETH payout is stuck because it uses too much gas. https:\/\/tinyurl.com\/y83dn2yf\/. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_3_1","volume-title":"https:\/\/github.com\/trailofbits\/manticore\/. [Online","year":"2019","unstructured":"2016. Manticore. https:\/\/github.com\/trailofbits\/manticore\/. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_4_1","volume-title":"On the parity wallet multisig hack. https:\/\/tinyurl.com\/yca83zsg\/. [Online","year":"2019","unstructured":"2017. On the parity wallet multisig hack. https:\/\/tinyurl.com\/yca83zsg\/. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_5_1","volume-title":"The Racket Language. https:\/\/racket-lang.org\/. [Online","year":"2019","unstructured":"2017. The Racket Language. https:\/\/racket-lang.org\/. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_6_1","volume-title":"Understanding The DAO Attack. https:\/\/tinyurl.com\/yc3o8ffk\/. [Online","year":"2019","unstructured":"2017. Understanding The DAO Attack. https:\/\/tinyurl.com\/yc3o8ffk\/. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_7_1","volume-title":"ETHEREUM: A SECURE DECENTRALISED GENERALISED TRANSACTION LEDGER. https:\/\/ethereum.github.io\/yellowpaper\/paper.pdf. [Online","year":"2019","unstructured":"2018. ETHEREUM: A SECURE DECENTRALISED GENERALISED TRANSACTION LEDGER. https:\/\/ethereum.github.io\/yellowpaper\/paper.pdf. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_8_1","volume-title":"The Ethereum Smart Contract Fuzzer for Security Vulnerability Detection. https:\/\/github.com\/gongbell\/ContractFuzzer. [Online","year":"2019","unstructured":"2018. The Ethereum Smart Contract Fuzzer for Security Vulnerability Detection. https:\/\/github.com\/gongbell\/ContractFuzzer. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_9_1","volume-title":"The Ethereum Smart Contract Fuzzer for Security Vulnerability Detection. https:\/\/github.com\/gongbell\/ContractFuzzer. [Online","year":"2019","unstructured":"2018. The Ethereum Smart Contract Fuzzer for Security Vulnerability Detection. https:\/\/github.com\/gongbell\/ContractFuzzer. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_10_1","volume-title":"Ethereum Smart Contract Security Best Practices. https:\/\/consensys.github.io\/smart-contract-best-practices\/. [Online","year":"2019","unstructured":"2018. Ethereum Smart Contract Security Best Practices. https:\/\/consensys.github.io\/smart-contract-best-practices\/. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_11_1","volume-title":"https:\/\/etherscan.io\/. [Online","year":"2019","unstructured":"2018. Etherscan. https:\/\/etherscan.io\/. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_12_1","volume-title":"https:\/\/github.com\/ConsenSys\/mythril-classic. [Online","author":"Classic Mythril","year":"2018","unstructured":"2018. Mythril Classic. https:\/\/github.com\/ConsenSys\/mythril-classic. [Online; accessed 12\/01\/2018]."},{"key":"e_1_3_2_1_13_1","volume-title":"New batchOverflow Bug in Multiple ERC20 Smart Contracts. https:\/\/tinyurl.com\/yd78gpyt. [Online","year":"2019","unstructured":"2018. New batchOverflow Bug in Multiple ERC20 Smart Contracts. https:\/\/tinyurl.com\/yd78gpyt. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_14_1","volume-title":"Parity Multisig Wallet Hacked, or How Come? https:\/\/cointelegraph.com\/news\/parity-multisig-wallet-hacked-or-how-come. [Online","year":"2019","unstructured":"2018. Parity Multisig Wallet Hacked, or How Come? https:\/\/cointelegraph.com\/news\/parity-multisig-wallet-hacked-or-how-come. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_15_1","volume-title":"Real Estate Business Integrates Smart Contracts. https:\/\/tinyurl.com\/yawrkfpx\/. [Online","year":"2019","unstructured":"2018. Real Estate Business Integrates Smart Contracts. https:\/\/tinyurl.com\/yawrkfpx\/. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_16_1","volume-title":"Smart contracts for shipping offer shortcut. https:\/\/tinyurl.com\/yavel7xe\/. [Online","year":"2019","unstructured":"2018. Smart contracts for shipping offer shortcut. https:\/\/tinyurl.com\/yavel7xe\/. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_17_1","volume-title":"Time manipulation. https:\/\/dasp.co\/. [Online","year":"2019","unstructured":"2018. Time manipulation. https:\/\/dasp.co\/. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_18_1","volume-title":"Unchecked Return Values For Low Level Calls. https:\/\/dasp.co. [Online","year":"2019","unstructured":"2018. Unchecked Return Values For Low Level Calls. https:\/\/dasp.co. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_19_1","volume-title":"https:\/\/bitcoin.org\/. [Online","year":"2019","unstructured":"2019. Bitcoin. https:\/\/bitcoin.org\/. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_20_1","volume-title":"https:\/\/www.ethereum.org\/. [Online","year":"2019","unstructured":"2019. Ethereum. https:\/\/www.ethereum.org\/. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_21_1","volume-title":"Ethereum Yellow Paper. https:\/\/github.com\/ethereum\/yellowpaper. [Online","year":"2019","unstructured":"2019. Ethereum Yellow Paper. https:\/\/github.com\/ethereum\/yellowpaper. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_22_1","volume-title":"https:\/\/github.com\/ethereum\/serpent. [Online","year":"2019","unstructured":"2019. Serpent. https:\/\/github.com\/ethereum\/serpent. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_23_1","volume-title":"https:\/\/solidity.readthedocs.io\/en\/v0.5.1\/. [Online","year":"2019","unstructured":"2019. Solidity. https:\/\/solidity.readthedocs.io\/en\/v0.5.1\/. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_24_1","volume-title":"https:\/\/github.com\/ethereum\/vyper. [Online","year":"2019","unstructured":"2019. Vyper. https:\/\/github.com\/ethereum\/vyper. [Online; accessed 01\/09\/2019]."},{"key":"e_1_3_2_1_25_1","unstructured":"Rajeev Alur Rastislav Bod\u00edk Eric Dallal Dana Fisman Pranav Garg Garvit Juniwal Hadas Kress-Gazit P. Madhusudan Milo M. K. Martin Mukund Raghothaman Shambwaditya Saha Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2015. Syntax-Guided Synthesis. In Dependable Software Systems Engineering. 1--25."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_28"},{"key":"e_1_3_2_1_27_1","volume-title":"POST 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22--29, 2017, Proceedings. 164--186","author":"Atzei Nicola","year":"2017","unstructured":"Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. 2017. A Survey of Attacks on Ethereum Smart Contracts (SoK). In Principles of Security and Trust - 6th International Conference, POST 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22--29, 2017, Proceedings. 164--186."},{"key":"e_1_3_2_1_28_1","volume-title":"Proc. The Network and Distributed System Security Symposium.","author":"Avgerinos Thanassis","year":"2011","unstructured":"Thanassis Avgerinos, Sang Kil Cha, Brent Lim Tze Hao, and David Brumley. 2011. AEG: Automatic Exploit Generation. In Proc. The Network and Distributed System Security Symposium."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_27"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.31"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190226"},{"key":"e_1_3_2_1_34_1","first-page":"1","article-title":"MadMax: surviving out-of-gas conditions in Ethereum smart contracts. In Proc. International Conference on Object-Oriented Programming","volume":"116","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. In Proc. International Conference on Object-Oriented Programming, Systems, Languages, and Applications. 116:1--116:27.","journal-title":"Systems, Languages, and Applications."},{"key":"e_1_3_2_1_35_1","volume-title":"POST 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14--20, 2018, Proceedings. 243--269","author":"Grishchenko Ilya","year":"2018","unstructured":"Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018. A Semantic Framework for the Security Analysis of Ethereum Smart Contracts. In Principles of Security and Trust - 7th International Conference, POST 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14--20, 2018, Proceedings. 243--269."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158136"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_3_2_1_38_1","volume-title":"Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In Financial Cryptography and Data Security - FC 2017 International Workshops, WAHC, BITCOIN, VOTING, WTSC, and TA, Sliema","author":"Hirai Yoichi","year":"2017","unstructured":"Yoichi Hirai. 2017. Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In Financial Cryptography and Data Security - FC 2017 International Workshops, WAHC, BITCOIN, VOTING, WTSC, and TA, Sliema, Malta, April 7, 2017, Revised Selected Papers. 520--535."},{"key":"e_1_3_2_1_39_1","volume-title":"Proc. International Conference on Automated Software Engineering. 259--269","author":"Jiang Bo","unstructured":"Bo Jiang, Ye Liu, and W. K. Chan. 2018. ContractFuzzer: fuzzing smart contracts for vulnerability detection. In Proc. International Conference on Automated Software Engineering. 259--269."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2018.23082"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_42_1","volume-title":"Proc. USENIX Security Symposium. 1317--1333","author":"Krupp Johannes","year":"2018","unstructured":"Johannes Krupp and Christian Rossow. 2018. teEther: Gnawing at Ethereum to Automatically Exploit Smart Contracts. In Proc. USENIX Security Symposium. 1317--1333."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Aina Niemetz Mathias Preiner and Armin Biere. 2014 (published 2015). Boolector 2.0 system description. Journal on Satisfiability Boolean Modeling and Computation 9 (2014 (published 2015)) 53--58.","DOI":"10.3233\/SAT190101"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3264591"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_2_1_48_1","volume-title":"Proc. Conference on Computer and Communications Security. 67--82","author":"Tsankov Petar","unstructured":"Petar Tsankov, Andrei Marian Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian B\u00fcnzli, and Martin T. Vechev. 2018. Securify: Practical Security Analysis of Smart Contracts. In Proc. Conference on Computer and Communications Security. 67--82."}],"event":{"name":"ASE '20: 35th IEEE\/ACM International Conference on Automated Software Engineering","location":"Virtual Event Australia","acronym":"ASE '20","sponsor":["SIGAI ACM Special Interest Group on Artificial Intelligence","SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"]},"container-title":["Proceedings of the 35th IEEE\/ACM International Conference on Automated Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3324884.3416646","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3324884.3416646","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:23Z","timestamp":1750193243000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3324884.3416646"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,12,21]]},"references-count":48,"alternative-id":["10.1145\/3324884.3416646","10.1145\/3324884"],"URL":"https:\/\/doi.org\/10.1145\/3324884.3416646","relation":{},"subject":[],"published":{"date-parts":[[2020,12,21]]},"assertion":[{"value":"2021-01-27","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}