{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,23]],"date-time":"2026-04-23T10:10:48Z","timestamp":1776939048410,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":75,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,6,11]],"date-time":"2020-06-11T00:00:00Z","timestamp":1591833600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["678177"],"award-info":[{"award-number":["678177"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,6,11]]},"DOI":"10.1145\/3385412.3386022","type":"proceedings-article","created":{"date-parts":[[2020,6,7]],"date-time":"2020-06-07T01:40:10Z","timestamp":1591494010000},"page":"470-486","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Behavioral simulation for smart contracts"],"prefix":"10.1145","author":[{"given":"Sidi Mohamed","family":"Beillahi","sequence":"first","affiliation":[{"name":"University of Paris Diderot, France \/ IRIF, France \/ CNRS, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriela","family":"Ciocarlie","sequence":"additional","affiliation":[{"name":"SRI International, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Emmi","sequence":"additional","affiliation":[{"name":"SRI International, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[{"name":"University of Paris Diderot, France \/ IRIF, France \/ CNRS, France \/ IUF, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,6,11]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"theDAO. https:\/\/etherscan.io\/address\/ 0xbb9bc244d798123fde783fcc1c72d3bb8c189413","year":"2017","unstructured":"2016. theDAO. https:\/\/etherscan.io\/address\/ 0xbb9bc244d798123fde783fcc1c72d3bb8c189413 2017. Blockchain is empowering the future of insurance. https:\/\/techcrunch.com\/2016\/10\/29\/blockchain-is-empoweringthe-future-of-insurance\/ 2017. An In-Depth Look at the Parity Multisig Bug. http:\/\/ hackxingdistributed.com\/2017\/07\/22\/deep-dive-parity-bug 2017. Northern Trust uses blockchain for private equity recordkeeping. http:\/\/www.reuters.com\/article\/nthern-trust-ibm-blockchainidUSL1N1G61TX. 2017. Parity security alert. https:\/\/www.parity.io\/security-alert-2\/ 2020. ERC-20 Token Standard. https:\/\/eips.ethereum.org\/EIPS\/eip-20"},{"key":"e_1_3_2_1_2_1","unstructured":"0xcert. 2019. https:\/\/github.com\/0xcert"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_10"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167084"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.DISC.2019.2"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_3_2_1_7_1","volume-title":"Zuck","author":"Barrett Clark W.","year":"2005","unstructured":"Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, and Lenore D. Zuck. 2005."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_29"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"e_1_3_2_1_10_1","unstructured":"Smart Contracts Benchmark. 2019. https:\/\/github.com\/beillahi\/smartcontract-simulation-data"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993611"},{"key":"e_1_3_2_1_12_1","unstructured":"BitNation. 2019. https:\/\/github.com\/Bit-Nation"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/635499.635502"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005069"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","unstructured":"10.3233\/JCS-2009-0393 10.3233\/JCS-2009-0393","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_2_1_17_1","unstructured":"Awesome CryptoKitties. 2019. https:\/\/github.com\/cryptocopycats"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380364"},{"key":"e_1_3_2_1_19_1","volume-title":"https:\/\/etherscan.io Retrieved November 19th","year":"2019","unstructured":"Etherscan. 2019. https:\/\/etherscan.io Retrieved November 19th, 2019."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_11"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_42"},{"key":"e_1_3_2_1_22_1","volume-title":"CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II (Lecture Notes in Computer Science), Swarat Chaudhuri and Azadeh Farzan (Eds.)","volume":"9780","author":"Fedyukovich Grigory","year":"2016","unstructured":"Grigory Fedyukovich, Arie Gurfinkel, and Natasha Sharygina. 2016. Property Directed Equivalence via Abstract Simulation. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II (Lecture Notes in Computer Science), Swarat Chaudhuri and Azadeh Farzan (Eds.), Vol. 9780."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","unstructured":"Springer 433\u2013453. 10.1007\/978-3-319-41540-6_24","DOI":"10.1007\/978-3-319-41540-6_24"},{"key":"e_1_3_2_1_24_1","unstructured":"Ganache. 2019. https:\/\/www.trufflesuite.com\/docs\/ganache\/overview"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1027328830731"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/ext066"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_17"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276486"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89722-6_10"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158136"},{"key":"e_1_3_2_1_34_1","volume-title":"solc-verify: A Modular Verifier for Solidity Smart Contracts. CoRR abs\/1907.04262","author":"Hajdu \u00c1kos","year":"2019","unstructured":"\u00c1kos Hajdu and Dejan Jovanovic. 2019. solc-verify: A Modular Verifier for Solidity Smart Contracts. CoRR abs\/1907.04262 (2019)."},{"key":"e_1_3_2_1_35_1","unstructured":"arXiv: 1907.04262 http:\/\/arxiv.org\/abs\/1907.04262"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363230"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1995.492576"},{"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","volume":"10323","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 (Lecture Notes in Computer Science), Michael Brenner, Kurt Rohloff, Joseph Bonneau, Andrew Miller, Peter Y. A. Ryan, Vanessa Teague, Andrea Bracciali, Massimiliano Sala, Federico Pintore, and Markus Jakobsson (Eds.), Vol. 10323."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","unstructured":"Springer 520\u2013535. 10.1007\/978-3-319-70278-0_33","DOI":"10.1007\/978-3-319-70278-0_33"},{"key":"e_1_3_2_1_40_1","volume-title":"ZEUS: Analyzing Safety of Smart Contracts. In 25th Annual Network and Distributed System Security Symposium, NDSS 2018","author":"Kalra Sukrit","year":"2018","unstructured":"Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. 2018. ZEUS: Analyzing Safety of Smart Contracts. In 25th Annual Network and Distributed System Security Symposium, NDSS 2018, San Diego, California, USA, February 18-21, 2018. The Internet Society. http:\/\/wp.internetsociety.org\/ndss\/wp-content\/uploads\/sites\/ 25\/2018\/02\/ndss2018_09-1_Kalra_paper.pdf"},{"key":"e_1_3_2_1_41_1","volume-title":"27th USENIX Security Symposium, USENIX Security 2018","author":"Krupp Johannes","year":"2018","unstructured":"Johannes Krupp and Christian Rossow. 2018. teEther: Gnawing at Ethereum to Automatically Exploit Smart Contracts. In 27th USENIX Security Symposium, USENIX Security 2018, Baltimore, MD, USA, August 15-17, 2018, William Enck and Adrienne Porter Felt (Eds.). USENIX Association, 1317\u20131333."},{"key":"e_1_3_2_1_42_1","unstructured":"https:\/\/www.usenix.org\/conference\/ usenixsecurity18\/presentation\/krupp"},{"key":"e_1_3_2_1_43_1","volume-title":"Formal Specification and Verification of Smart Contracts for Azure Blockchain. CoRR abs\/1812.08829","author":"Lahiri Shuvendu K.","year":"2018","unstructured":"Shuvendu K. Lahiri, Shuo Chen, Yuepeng Wang, and Isil Dillig. 2018. Formal Specification and Verification of Smart Contracts for Azure Blockchain. CoRR abs\/1812.08829 (2018). arXiv: 1812.08829 http: \/\/arxiv.org\/abs\/1812.08829"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"e_1_3_2_1_47_1","volume-title":"Communication and concurrency","author":"Milner Robin","unstructured":"Robin Milner. 1989. Communication and concurrency. Prentice Hall."},{"key":"e_1_3_2_1_48_1","volume-title":"Machine learning","author":"Mitchell Tom M.","unstructured":"Tom M. Mitchell. 1997. Machine learning. McGraw-Hill. http:\/\/www. worldcat.org\/oclc\/61321007"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40787-1_22"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_17"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274743"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","unstructured":"ACM 653\u2013663. 10.1145\/3274694.3274743","DOI":"10.1145\/3274694.3274743"},{"key":"e_1_3_2_1_54_1","unstructured":"State of the DApps. 2019. https:\/\/www.stateofthedapps.com"},{"key":"e_1_3_2_1_55_1","unstructured":"OpenZeppelin. 2019. https:\/\/github.com\/OpenZeppelin"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_3_2_1_57_1","volume-title":"VerX: Safety Verification of Smart Contracts. In IEEE Symposium on Security and Privacy (SP","author":"Permenev Anton","year":"2020","unstructured":"Anton Permenev, Dimitar Dimitrov, Petar Tsankov, Dana Drachsler-Chohen, and Martin Vechev. 2020. VerX: Safety Verification of Smart Contracts. In IEEE Symposium on Security and Privacy (SP 2020)."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.06.002"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390666"},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03427-6_25"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_11"},{"key":"e_1_3_2_1_62_1","unstructured":"Sirin-labs. 2019. https:\/\/github.com\/sirin-labs"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_1_64_1","volume-title":"https:\/\/solidity.readthedocs.io\/en\/v0.4.24\/solidity-byexample.html#blind-auction Retrieved November 19th","year":"2019","unstructured":"Solidity. 2019. https:\/\/solidity.readthedocs.io\/en\/v0.4.24\/solidity-byexample.html#blind-auction Retrieved November 19th, 2019."},{"key":"e_1_3_2_1_65_1","unstructured":"the Contract-Oriented Programming Language Solidity. 2019. https: \/\/solidity.readthedocs.io\/en\/v0.5.0\/"},{"key":"e_1_3_2_1_66_1","unstructured":"Paxos Standard ERC20 stablecoin PAX. 2019."},{"key":"e_1_3_2_1_67_1","unstructured":"https:\/\/github.com\/paxosglobal\/pax-contracts\/blob\/ 3d50aa32c4691c46d2bf3f8150fff270849e8dbe\/contracts\/ PAXImplementation.sol Retrieved November 19th 2019."},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363222"},{"key":"e_1_3_2_1_69_1","unstructured":"Sergei Tikhomirov Ekaterina Voskresenskaya Ivan Ivanitskiy Ramil Takhaviev Evgeny Marchenko and Yaroslav Alexandrov. 2018."},{"key":"e_1_3_2_1_70_1","volume-title":"1st IEEE\/ACM International Workshop on Emerging Trends in Software Engineering for Blockchain, WETSEB@ICSE 2018","year":"2018","unstructured":"SmartCheck: Static Analysis of Ethereum Smart Contracts. In 1st IEEE\/ACM International Workshop on Emerging Trends in Software Engineering for Blockchain, WETSEB@ICSE 2018, Gothenburg, Sweden, May 27 - June 3, 2018. ACM, 9\u201316. http:\/\/ieeexplore.ieee.org\/document\/ 8445052"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274737"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993533"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243780"},{"key":"e_1_3_2_1_74_1","unstructured":"Moloch Ventures. 2019. https:\/\/github.com\/MolochVentures"},{"key":"e_1_3_2_1_75_1","unstructured":"web3.js Ethereum JavaScript API. 2019. https:\/\/web3js.readthedocs. io\/en\/v1.2.4\/"}],"event":{"name":"PLDI '20: 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"London UK","acronym":"PLDI '20","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3386022","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3385412.3386022","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:38:49Z","timestamp":1750199929000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3385412.3386022"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,11]]},"references-count":75,"alternative-id":["10.1145\/3385412.3386022","10.1145\/3385412"],"URL":"https:\/\/doi.org\/10.1145\/3385412.3386022","relation":{},"subject":[],"published":{"date-parts":[[2020,6,11]]},"assertion":[{"value":"2020-06-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}