{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,1]],"date-time":"2026-03-01T05:41:11Z","timestamp":1772343671231,"version":"3.50.1"},"reference-count":191,"publisher":"Association for Computing Machinery (ACM)","issue":"7","license":[{"start":{"date-parts":[[2021,7,18]],"date-time":"2021-07-18T00:00:00Z","timestamp":1626566400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001381","name":"National Research Foundation Singapore","doi-asserted-by":"publisher","award":["NRF2017EWT-EP003-023"],"award-info":[{"award-number":["NRF2017EWT-EP003-023"]}],"id":[{"id":"10.13039\/501100001381","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001459","name":"Ministry of Education, Singapore","doi-asserted-by":"crossref","award":["2018-T1-002-069, MOE2018-T2-1-068"],"award-info":[{"award-number":["2018-T1-002-069, MOE2018-T2-1-068"]}],"id":[{"id":"10.13039\/501100001459","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001447","name":"Energy Market Authority of Singapore","doi-asserted-by":"publisher","award":["NRF2017EWT-EP003-023"],"award-info":[{"award-number":["NRF2017EWT-EP003-023"]}],"id":[{"id":"10.13039\/501100001447","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2022,9,30]]},"abstract":"<jats:p>A smart contract is a computer program that allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain, finance, legal, and medical services, there is a strong demand for verification and validation techniques. Yet, the vast majority of smart contracts lack any kind of formal specification, which is essential for establishing their correctness. In this survey, we investigate formal models and specifications of smart contracts presented in the literature and present a systematic overview to understand the common trends. We also discuss the current approaches used in verifying such property specifications and identify gaps with the hope to recognize promising directions for future work.<\/jats:p>","DOI":"10.1145\/3464421","type":"journal-article","created":{"date-parts":[[2021,7,18]],"date-time":"2021-07-18T16:07:33Z","timestamp":1626624453000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":186,"title":["A Survey of Smart Contract Formal Specification and Verification"],"prefix":"10.1145","volume":"54","author":[{"given":"Palina","family":"Tolmach","sequence":"first","affiliation":[{"name":"Nanyang Technological University, Singapore and Institute of High Performance Computing (A*STAR), Singapore"}]},{"given":"Yi","family":"Li","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}]},{"given":"Shang-Wei","family":"Lin","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}]},{"given":"Zengxiang","family":"Li","sequence":"additional","affiliation":[{"name":"Institute of High Performance Computing (A*STAR), Singapore"}]}],"member":"320","published-online":{"date-parts":[[2021,7,18]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2016. King of the Ether Throne \u2014 Post-Mortem Investigation. Retrieved from https:\/\/www.kingoftheether.com\/postmortem.html.  2016. King of the Ether Throne \u2014 Post-Mortem Investigation. Retrieved from https:\/\/www.kingoftheether.com\/postmortem.html."},{"key":"e_1_2_1_2_1","unstructured":"2018. Bamboo: A Morphing Smart Contract Language. Retrieved from https:\/\/github.com\/cornellblockchain\/bamboo.  2018. Bamboo: A Morphing Smart Contract Language. Retrieved from https:\/\/github.com\/cornellblockchain\/bamboo."},{"key":"e_1_2_1_3_1","unstructured":"2020. Common Patterns \u2014 Solidity 0.6.11 documentation. Retrieved from https:\/\/solidity.readthedocs.io\/en\/v0.6.11\/common-patterns.html.  2020. Common Patterns \u2014 Solidity 0.6.11 documentation. Retrieved from https:\/\/solidity.readthedocs.io\/en\/v0.6.11\/common-patterns.html."},{"key":"e_1_2_1_4_1","unstructured":"2020. EOS.IO Technical White Paper v2. Retrieved from https:\/\/github.com\/EOSIO\/Documentation\/blob\/master\/TechnicalWhitePaper.md.  2020. EOS.IO Technical White Paper v2. Retrieved from https:\/\/github.com\/EOSIO\/Documentation\/blob\/master\/TechnicalWhitePaper.md."},{"key":"e_1_2_1_5_1","volume-title":"Retrieved","year":"2020","unstructured":"Etherscan. 2020 . Ethereum Charts and Statistics | Etherscan . Retrieved February 13, 2020 from https:\/\/etherscan.io\/charts. Etherscan. 2020. Ethereum Charts and Statistics | Etherscan. Retrieved February 13, 2020 from https:\/\/etherscan.io\/charts."},{"key":"e_1_2_1_6_1","unstructured":"2020. Solidity \u2014 Solidity 0.6.11 documentation. Retrieved from https:\/\/solidity.readthedocs.io\/en\/v0.6.11\/.  2020. Solidity \u2014 Solidity 0.6.11 documentation. Retrieved from https:\/\/solidity.readthedocs.io\/en\/v0.6.11\/."},{"key":"e_1_2_1_7_1","unstructured":"2020. Solidity by Example \u2014 Solidity 0.6.11 documentation. Retrieved from https:\/\/solidity.readthedocs.io\/en\/v0.6.11\/solidity-by-example.html.  2020. Solidity by Example \u2014 Solidity 0.6.11 documentation. Retrieved from https:\/\/solidity.readthedocs.io\/en\/v0.6.11\/solidity-by-example.html."},{"key":"e_1_2_1_8_1","unstructured":"2021. Daml Programming Language. Retrieved from https:\/\/daml.com.  2021. Daml Programming Language. Retrieved from https:\/\/daml.com."},{"key":"e_1_2_1_9_1","unstructured":"2021. Transaction execution approval language (TEAL) specification. Retrieved from https:\/\/developer.algorand.org\/docs\/reference\/teal\/specification.  2021. Transaction execution approval language (TEAL) specification. Retrieved from https:\/\/developer.algorand.org\/docs\/reference\/teal\/specification."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the IFIP NTMS. IEEE, 1\u20135.","author":"Abdellatif T.","unstructured":"T. Abdellatif and K. L. Brousmiche . 2018. Formal verification of smart contracts based on users and blockchain behaviors models . In Proceedings of the IFIP NTMS. IEEE, 1\u20135. T. Abdellatif and K. L. Brousmiche. 2018. Formal verification of smart contracts based on users and blockchain behaviors models. In Proceedings of the IFIP NTMS. IEEE, 1\u20135."},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the FSEN. Springer International Publishing, Cham, 228\u2013243","author":"Ahrendt W.","unstructured":"W. Ahrendt , R. Bubel , J. Ellul , G. J. Pace , R. Pardo , V. Rebiscoul , and G. Schneider . 2019. Verification of smart contract business logic . In Proceedings of the FSEN. Springer International Publishing, Cham, 228\u2013243 . W. Ahrendt, R. Bubel, J. Ellul, G. J. Pace, R. Pardo, V. Rebiscoul, and G. Schneider. 2019. Verification of smart contract business logic. In Proceedings of the FSEN. Springer International Publishing, Cham, 228\u2013243."},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the APSEC. 482\u2013489","author":"Akca S.","unstructured":"S. Akca , A. Rajan , and C. Peng . 2019. SolAnalyser: A framework for analysing and testing smart contracts . In Proceedings of the APSEC. 482\u2013489 . S. Akca, A. Rajan, and C. Peng. 2019. SolAnalyser: A framework for analysing and testing smart contracts. In Proceedings of the APSEC. 482\u2013489."},{"key":"e_1_2_1_13_1","volume-title":"GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. arxiv:1912.11929.","author":"Albert E.","year":"2019","unstructured":"E. Albert , J. Correas , P. Gordillo , G. Rom\u00e1n-D\u00edez , and A. Rubio . 2019 . GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. arxiv:1912.11929. E. Albert, J. Correas, P. Gordillo, G. Rom\u00e1n-D\u00edez, and A. Rubio. 2019. GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. arxiv:1912.11929."},{"key":"e_1_2_1_14_1","volume-title":"SAFEVM: A safety verifier for ethereum smart contracts. CoRR abs\/1906.04984","author":"Albert E.","year":"2019","unstructured":"E. Albert , J. Correas , P. Gordillo , G. Rom\u00e1n-D\u00edez , and A. Rubio . 2019 . SAFEVM: A safety verifier for ethereum smart contracts. CoRR abs\/1906.04984 (2019). E. Albert, J. Correas, P. Gordillo, G. Rom\u00e1n-D\u00edez, and A. Rubio. 2019. SAFEVM: A safety verifier for ethereum smart contracts. CoRR abs\/1906.04984 (2019)."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the HICSS.","author":"Alqahtani S.","unstructured":"S. Alqahtani , X. He , R. Gamble , and P. Mauricio . 2020. Formal verification of functional requirements for smart contract compositions in supply chain management systems . In Proceedings of the HICSS. S. Alqahtani, X. He, R. Gamble, and P. Mauricio. 2020. Formal verification of functional requirements for smart contract compositions in supply chain management systems. In Proceedings of the HICSS."},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the ACM CPP. ACM Press, 66\u201377","author":"Amani S.","unstructured":"S. Amani , M. B\u00e9gel , M. Bortin , and M. Staples . 2018. Towards verifying ethereum smart contract bytecode in Isabelle\/HOL . In Proceedings of the ACM CPP. ACM Press, 66\u201377 . S. Amani, M. B\u00e9gel, M. Bortin, and M. Staples. 2018. Towards verifying ethereum smart contract bytecode in Isabelle\/HOL. In Proceedings of the ACM CPP. ACM Press, 66\u201377."},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the EuroSys. ACM.","author":"Androulaki E.","unstructured":"E. Androulaki , A. Barger , V. Bortnikov , C. Cachin , K. Christidis , A. De Caro , D. Enyeart , C. Ferris , G. Laventman , and Y. Manevich . 2018. Hyperledger fabric: A distributed operating system for permissioned blockchains . In Proceedings of the EuroSys. ACM. E. Androulaki, A. Barger, V. Bortnikov, C. Cachin, K. Christidis, A. De Caro, D. Enyeart, C. Ferris, G. Laventman, and Y. Manevich. 2018. Hyperledger fabric: A distributed operating system for permissioned blockchains. In Proceedings of the EuroSys. ACM."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10512-3_2"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the ACM CCP. ACM, 215\u2014228","author":"Annenkov D.","unstructured":"D. Annenkov , J. B. Nielsen , and B. Spitters . 2020. ConCert: A smart contract certification framework in coq . In Proceedings of the ACM CCP. ACM, 215\u2014228 . D. Annenkov, J. B. Nielsen, and B. Spitters. 2020. ConCert: A smart contract certification framework in coq. In Proceedings of the ACM CCP. ACM, 215\u2014228."},{"key":"e_1_2_1_20_1","volume-title":"Solidifier: A bounded model checker for Solidity. arxiv:2002.02710.","author":"Antonino P.","year":"2020","unstructured":"P. Antonino and A. W. Roscoe . 2020 . Formalising and verifying smart contracts with Solidifier: A bounded model checker for Solidity. arxiv:2002.02710. P. Antonino and A. W. Roscoe. 2020. Formalising and verifying smart contracts with Solidifier: A bounded model checker for Solidity. arxiv:2002.02710."},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"A. W. Appel R. Dockins A. Hobor L. Beringer J. Dodds G. Stewart S. Blazy and X. Leroy. 2014. Program Logics for Certified Compilers. Cambridge University Press.  A. W. Appel R. Dockins A. Hobor L. Beringer J. Dodds G. Stewart S. Blazy and X. Leroy. 2014. Program Logics for Certified Compilers. Cambridge University Press.","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_2_1_22_1","unstructured":"A. Arusoaie. 2020. Certifying Findel Derivatives for Blockchain. arxiv:2005.13602.  A. Arusoaie. 2020. Certifying Findel Derivatives for Blockchain. arxiv:2005.13602."},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the POST. Springer, 164\u2013186","author":"Atzei N.","unstructured":"N. Atzei , M. Bartoletti , and T. Cimoli . 2017. A survey of attacks on ethereum smart contracts . In Proceedings of the POST. Springer, 164\u2013186 . N. Atzei, M. Bartoletti, and T. Cimoli. 2017. A survey of attacks on ethereum smart contracts. In Proceedings of the POST. Springer, 164\u2013186."},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the POST. Springer International Publishing, 217\u2013242","author":"Atzei N.","unstructured":"N. Atzei , M. Bartoletti , T. Cimoli , S. Lande , and R. Zunino . 2018. SoK: Unraveling bitcoin smart contracts . In Proceedings of the POST. Springer International Publishing, 217\u2013242 . N. Atzei, M. Bartoletti, T. Cimoli, S. Lande, and R. Zunino. 2018. SoK: Unraveling bitcoin smart contracts. In Proceedings of the POST. Springer International Publishing, 217\u2013242."},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the ACM ESEC\/FSE. ACM, 1124\u20131128","author":"Atzei N.","unstructured":"N. Atzei , M. Bartoletti , S. Lande , N. Yoshida , and R. Zunino . 2019. Developing secure bitcoin contracts with BitML . In Proceedings of the ACM ESEC\/FSE. ACM, 1124\u20131128 . N. Atzei, M. Bartoletti, S. Lande, N. Yoshida, and R. Zunino. 2019. Developing secure bitcoin contracts with BitML. In Proceedings of the ACM ESEC\/FSE. ACM, 1124\u20131128."},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the RV","volume":"11237","author":"Azzopardi S.","unstructured":"S. Azzopardi , J. Ellul , and G. J. Pace . 2019. Monitoring smart contracts: ContractLarva and open challenges beyond . In Proceedings of the RV , Vol. 11237 . Springer Verlag, 113\u2013137. S. Azzopardi, J. Ellul, and G. J. Pace. 2019. Monitoring smart contracts: ContractLarva and open challenges beyond. In Proceedings of the RV, Vol. 11237. Springer Verlag, 113\u2013137."},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the JURIX","volume":"313","author":"Azzopardi S.","unstructured":"S. Azzopardi , G. J. Pace , and F. Schapachnik . 2018. On observing contracts: Deontic contracts meet smart contracts . In Proceedings of the JURIX , Vol. 313 . IOS Press, 21\u201330. S. Azzopardi, G. J. Pace, and F. Schapachnik. 2018. On observing contracts: Deontic contracts meet smart contracts. In Proceedings of the JURIX, Vol. 313. IOS Press, 21\u201330."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.036"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the ACM ICSCA. ACM Press, 322\u2013326","author":"Bai X.","unstructured":"X. Bai , Z. Cheng , Z. Duan , and K. Hu . 2018. Formal modeling and verification of smart contracts . In Proceedings of the ACM ICSCA. ACM Press, 322\u2013326 . X. Bai, Z. Cheng, Z. Duan, and K. Hu. 2018. Formal modeling and verification of smart contracts. In Proceedings of the ACM ICSCA. ACM Press, 322\u2013326."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-43725-1_9"},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the FC","volume":"10323","author":"Bartoletti M.","unstructured":"M. Bartoletti and L. Pompianu . 2017. An empirical analysis of smart contracts: Platforms, applications, and design patterns . In Proceedings of the FC , Vol. 10323 LNCS. Springer Verlag, 494\u2013509. arxiv:1703.06322. M. Bartoletti and L. Pompianu. 2017. An empirical analysis of smart contracts: Platforms, applications, and design patterns. In Proceedings of the FC, Vol. 10323 LNCS. Springer Verlag, 494\u2013509. arxiv:1703.06322."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.3389\/fbloc.2019.00008"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the POST. Springer International Publishing, 222\u2013247","author":"Bartoletti M.","unstructured":"M. Bartoletti and R. Zunino . 2019. Verifying liquidity of bitcoin contracts . In Proceedings of the POST. Springer International Publishing, 222\u2013247 . M. Bartoletti and R. Zunino. 2019. Verifying liquidity of bitcoin contracts. In Proceedings of the POST. Springer International Publishing, 222\u2013247."},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the SDLT.","author":"Beckert B.","unstructured":"B. Beckert , M. Herda , M. Kirsten , and J. Schiffl . 2018. Formal specification and verification of hyperledger fabric chaincode . In Proceedings of the SDLT. B. Beckert, M. Herda, M. Kirsten, and J. Schiffl. 2018. Formal specification and verification of hyperledger fabric chaincode. In Proceedings of the SDLT."},{"key":"e_1_2_1_35_1","volume-title":"Smart Contracts: Application Scenarios for Program Verification.","author":"Beckert B.","year":"2019","unstructured":"B. Beckert , J. Schiffl , and M. Ulbrich . 2019 . Smart Contracts: Application Scenarios for Program Verification. Retrieved from https:\/\/www.key-project.org\/wp-content\/uploads\/2019\/11\/sc-verification.pdf. B. Beckert, J. Schiffl, and M. Ulbrich. 2019. Smart Contracts: Application Scenarios for Program Verification. Retrieved from https:\/\/www.key-project.org\/wp-content\/uploads\/2019\/11\/sc-verification.pdf."},{"key":"e_1_2_1_36_1","volume-title":"WIP: Finding bugs automatically in smart contracts with parameterized invariants.","author":"Bernardi T.","year":"2020","unstructured":"T. Bernardi , N. Dor , A. Fedotov , S. Grossman , N. Immerman , D. Jackson , A. Nutz , L. Oppenheim , O. Pistiner , N. Rinetzky , M. Sagiv , M. Taube , J. A. Toman , and J. R. Wilcox . 2020 . WIP: Finding bugs automatically in smart contracts with parameterized invariants. Retrieved from https:\/\/www.certora.com\/pubs\/sbc2020.pdf. T. Bernardi, N. Dor, A. Fedotov, S. Grossman, N. Immerman, D. Jackson, A. Nutz, L. Oppenheim, O. Pistiner, N. Rinetzky, M. Sagiv, M. Taube, J. A. Toman, and J. R. Wilcox. 2020. WIP: Finding bugs automatically in smart contracts with parameterized invariants. Retrieved from https:\/\/www.certora.com\/pubs\/sbc2020.pdf."},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"B. Bernardo R. Cauderlier Z. Hu B. Pesin and J. Tesson. 2019. Mi-Cho-Coq a Framework for Certifying Tezos Smart Contracts. arxiv:1909.08671.  B. Bernardo R. Cauderlier Z. Hu B. Pesin and J. Tesson. 2019. Mi-Cho-Coq a Framework for Certifying Tezos Smart Contracts. arxiv:1909.08671.","DOI":"10.1007\/978-3-030-54994-7_28"},{"key":"e_1_2_1_38_1","doi-asserted-by":"crossref","unstructured":"B. Bernardo R. Cauderlier B. Pesin and J. Tesson. 2020. Albert an Intermediate Smart-Contract Language for the Tezos Blockchain. arxiv:2001.02630.  B. Bernardo R. Cauderlier B. Pesin and J. Tesson. 2020. Albert an Intermediate Smart-Contract Language for the Tezos Blockchain. arxiv:2001.02630.","DOI":"10.1007\/978-3-030-54455-3_41"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the ACM PLAS. ACM Press, 91\u201396","author":"Bhargavan K.","unstructured":"K. Bhargavan , N. Swamy , S. Zanella-B\u00e9guelin , A. Delignat-Lavaud , C. Fournet , A. Gollamudi , G. Gonthier , N. Kobeissi , N. Kulatova , A. Rastogi , and T. Sibut-Pinote . 2016. Formal verification of smart contracts . In Proceedings of the ACM PLAS. ACM Press, 91\u201396 . K. Bhargavan, N. Swamy, S. Zanella-B\u00e9guelin, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, and T. Sibut-Pinote. 2016. Formal verification of smart contracts. In Proceedings of the ACM PLAS. ACM Press, 91\u201396."},{"key":"e_1_2_1_40_1","doi-asserted-by":"crossref","unstructured":"G. Bigi A. Bracciali G. Meacci and E. Tuosto. 2015. Validation of Decentralised Smart Contracts Through Game Theory and Formal Methods. Springer International Publishing 142\u2013161.  G. Bigi A. Bracciali G. Meacci and E. Tuosto. 2015. Validation of Decentralised Smart Contracts Through Game Theory and Formal Methods. Springer International Publishing 142\u2013161.","DOI":"10.1007\/978-3-319-25527-9_11"},{"key":"e_1_2_1_41_1","volume-title":"Resources: A Safe Language Abstraction for Money. arxiv:2004.05106.","author":"Blackshear S.","year":"2020","unstructured":"S. Blackshear , D. L. Dill , S. Qadeer , C. W. Barrett , J. C. Mitchell , O. Padon , and Y. Zohar . 2020 . Resources: A Safe Language Abstraction for Money. arxiv:2004.05106. S. Blackshear, D. L. Dill, S. Qadeer, C. W. Barrett, J. C. Mitchell, O. Padon, and Y. Zohar. 2020. Resources: A Safe Language Abstraction for Money. arxiv:2004.05106."},{"key":"e_1_2_1_42_1","volume-title":"Proceedings of the IEEE IWBOSE. 9\u201318","author":"Bragagnolo S.","unstructured":"S. Bragagnolo , H. Rocha , M. Denker , and S. Ducasse . 2018. SmartInspect: Solidity smart contract inspector . In Proceedings of the IEEE IWBOSE. 9\u201318 . S. Bragagnolo, H. Rocha, M. Denker, and S. Ducasse. 2018. SmartInspect: Solidity smart contract inspector. In Proceedings of the IEEE IWBOSE. 9\u201318."},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the ACM PLDI. ACM, 454\u2013469","author":"Brent L.","unstructured":"L. Brent , N. Grech , S. Lagouvardos , B. Scholz , and Y. Smaragdakis . 2020. Ethainter: A smart contract security analyzer for composite vulnerabilities . In Proceedings of the ACM PLDI. ACM, 454\u2013469 . L. Brent, N. Grech, S. Lagouvardos, B. Scholz, and Y. Smaragdakis. 2020. Ethainter: A smart contract security analyzer for composite vulnerabilities. In Proceedings of the ACM PLDI. ACM, 454\u2013469."},{"key":"e_1_2_1_44_1","volume-title":"Vandal: A Scalable Security Analysis Framework for Smart Contracts. arxiv:1809.03981.","author":"Brent Lexi","year":"2018","unstructured":"Lexi Brent , Anton Jurisevic , Michael Kong , Eric Liu , Francois Gauthier , Vincent Gramoli , Ralph Holz , and Bernhard Scholz . 2018 . Vandal: A Scalable Security Analysis Framework for Smart Contracts. arxiv:1809.03981. Lexi Brent, Anton Jurisevic, Michael Kong, Eric Liu, Francois Gauthier, Vincent Gramoli, Ralph Holz, and Bernhard Scholz. 2018. Vandal: A Scalable Security Analysis Framework for Smart Contracts. arxiv:1809.03981."},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the ICFEM. Springer International Publishing, 286\u2013304","author":"Chang J.","unstructured":"J. Chang , B. Gao , H. Xiao , J. Sun , Y. Cai , and Z. Yang . 2019. sCompile: Critical path identification and analysis for smart contracts . In Proceedings of the ICFEM. Springer International Publishing, 286\u2013304 . J. Chang, B. Gao, H. Xiao, J. Sun, Y. Cai, and Z. Yang. 2019. sCompile: Critical path identification and analysis for smart contracts. In Proceedings of the ICFEM. Springer International Publishing, 286\u2013304."},{"key":"e_1_2_1_46_1","volume-title":"Proceedings of the MPC. Springer International Publishing, 255\u2013297","author":"Chapman J.","unstructured":"J. Chapman , R. Kireev , C. Nester , and P. Wadler . 2019. System F in Agda, for fun and profit . In Proceedings of the MPC. Springer International Publishing, 255\u2013297 . J. Chapman, R. Kireev, C. Nester, and P. Wadler. 2019. System F in Agda, for fun and profit. In Proceedings of the MPC. Springer International Publishing, 255\u2013297."},{"key":"e_1_2_1_47_1","volume-title":"Proceedings of the ESOP","volume":"10801","author":"Chatterjee K.","year":"1801","unstructured":"K. Chatterjee , A. K. Goharshady , and Y. Velner . 2018. Quantitative analysis of smart contracts . In Proceedings of the ESOP , Vol. 10801 LNCS. Springer Verlag, 739\u2013767. arxiv : 1801 .03367. K. Chatterjee, A. K. Goharshady, and Y. Velner. 2018. Quantitative analysis of smart contracts. In Proceedings of the ESOP, Vol. 10801 LNCS. Springer Verlag, 739\u2013767. arxiv:1801.03367."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3391195"},{"key":"e_1_2_1_49_1","unstructured":"J. Chen X. Xia D. Lo and J. Grundy. 2020. Why Do Smart Contracts Self-Destruct? Investigating the Selfdestruct Function on Ethereum. arxiv:2005.07908.  J. Chen X. Xia D. Lo and J. Grundy. 2020. Why Do Smart Contracts Self-Destruct? Investigating the Selfdestruct Function on Ethereum. arxiv:2005.07908."},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the NDSS.","author":"Chen T.","unstructured":"T. Chen , R. Cao , T. Li , X. Luo , G. Gu , Y. Zhang , Z. Liao , H. Zhu , G. Chen , Z. He , Y. Tang , X. Lin , and X. Zhang . 2020. SODA: A generic online detection framework for smart contracts . In Proceedings of the NDSS. T. Chen, R. Cao, T. Li, X. Luo, G. Gu, Y. Zhang, Z. Liao, H. Zhu, G. Chen, Z. He, Y. Tang, X. Lin, and X. Zhang. 2020. SODA: A generic online detection framework for smart contracts. In Proceedings of the NDSS."},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the IEEE SANER. 442\u2013446","author":"Chen T.","unstructured":"T. Chen , X. Li , X. Luo , and X. Zhang . 2017. Under-optimized smart contracts devour your money . In Proceedings of the IEEE SANER. 442\u2013446 . T. Chen, X. Li, X. Luo, and X. Zhang. 2017. Under-optimized smart contracts devour your money. In Proceedings of the IEEE SANER. 442\u2013446."},{"key":"e_1_2_1_52_1","volume-title":"Proceedings of the ACM CCS. ACM, 1503\u20131520","author":"Chen T.","unstructured":"T. Chen , Y. Zhang , Z. Li , X. Luo , T. Wang , R. Cao , X. Xiao , and X. Zhang . 2019. TokenScope: Automatically detecting inconsistent behaviors of cryptocurrency tokens in ethereum . In Proceedings of the ACM CCS. ACM, 1503\u20131520 . T. Chen, Y. Zhang, Z. Li, X. Luo, T. Wang, R. Cao, X. Xiao, and X. Zhang. 2019. TokenScope: Automatically detecting inconsistent behaviors of cryptocurrency tokens in ethereum. In Proceedings of the ACM CCS. ACM, 1503\u20131520."},{"key":"e_1_2_1_53_1","volume-title":"Proceedings of the WWW. ACM, 1411\u20131421","author":"Chen W.","unstructured":"W. Chen , T. Zhang , Z. Chen , Z. Zheng , and Y. Lu . 2020. Traveling the token world: A graph analysis of ethereum ERC20 token ecosystem . In Proceedings of the WWW. ACM, 1411\u20131421 . W. Chen, T. Zhang, Z. Chen, Z. Zheng, and Y. Lu. 2020. Traveling the token world: A graph analysis of ethereum ERC20 token ecosystem. In Proceedings of the WWW. ACM, 1411\u20131421."},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the ISoLA","volume":"11247","author":"Clack C. D.","year":"1805","unstructured":"C. D. Clack and G. Vanca . 2018. Temporal aspects of smart contracts for financial derivatives . In Proceedings of the ISoLA , Vol. 11247 LNCS. Springer Verlag, 339\u2013355. arxiv : 1805 .11677. C. D. Clack and G. Vanca. 2018. Temporal aspects of smart contracts for financial derivatives. In Proceedings of the ISoLA, Vol. 11247 LNCS. Springer Verlag, 339\u2013355. arxiv:1805.11677."},{"key":"e_1_2_1_55_1","volume-title":"Obsidian: Typestate and Assets for Safer Blockchain Programming. arxiv:1909.03523.","author":"Coblenz M.","year":"2019","unstructured":"M. Coblenz , R. Oei , T. Etzel , P. Koronkevich , M. Baker , Y. Bloem , B. A. Myers , J. Sunshine , and J. Aldrich . 2019 . Obsidian: Typestate and Assets for Safer Blockchain Programming. arxiv:1909.03523. M. Coblenz, R. Oei, T. Etzel, P. Koronkevich, M. Baker, Y. Bloem, B. A. Myers, J. Sunshine, and J. Aldrich. 2019. Obsidian: Typestate and Assets for Safer Blockchain Programming. arxiv:1909.03523."},{"key":"e_1_2_1_56_1","volume-title":"Proceedings of the ISoLA","volume":"11247","author":"Colombo C.","unstructured":"C. Colombo , J. Ellul , and G. J. Pace . 2018. Contracts over smart contracts: Recovering from violations dynamically . In Proceedings of the ISoLA , Vol. 11247 LNCS. Springer Verlag, 300\u2013315. C. Colombo, J. Ellul, and G. J. Pace. 2018. Contracts over smart contracts: Recovering from violations dynamically. In Proceedings of the ISoLA, Vol. 11247 LNCS. Springer Verlag, 300\u2013315."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.2307\/2082975"},{"key":"e_1_2_1_58_1","unstructured":"L. P. A. da Horta J. S. Reis M. Pereira and S. M. de Sousa. 2020. WhylSon: Proving your Michelson Smart Contracts in Why3. arxiv:2005.14650.  L. P. A. da Horta J. S. Reis M. Pereira and S. M. de Sousa. 2020. WhylSon: Proving your Michelson Smart Contracts in Why3. arxiv:2005.14650."},{"key":"e_1_2_1_59_1","volume-title":"Proceedings of the IEEE DAPPCON. IEEE, 69\u201378","author":"di Angelo M.","unstructured":"M. di Angelo and G. Salzer . 2019. A survey of tools for analyzing ethereum smart contracts . In Proceedings of the IEEE DAPPCON. IEEE, 69\u201378 . M. di Angelo and G. Salzer. 2019. A survey of tools for analyzing ethereum smart contracts. In Proceedings of the IEEE DAPPCON. IEEE, 69\u201378."},{"key":"e_1_2_1_60_1","volume-title":"Proceedings of the FC. Springer Berlin, 325\u2013338","author":"Dickerson T.","unstructured":"T. Dickerson , P. Gazzillo , M. Herlihy , V. Saraph , and E. Koskinen . 2019. Proof-carrying smart contracts . In Proceedings of the FC. Springer Berlin, 325\u2013338 . T. Dickerson, P. Gazzillo, M. Herlihy, V. Saraph, and E. Koskinen. 2019. Proof-carrying smart contracts. In Proceedings of the FC. Springer Berlin, 325\u2013338."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/MIS.2020.2977594"},{"key":"e_1_2_1_62_1","volume-title":"Proceedings of the IEEE\/ACM ICSE. arxiv:1910","author":"Durieux T.","unstructured":"T. Durieux , J. F. Ferreira , R. Abreu , and P. Cruz . 2020. Empirical review of automated analysis tools on 47,587 ethereum smart contracts . In Proceedings of the IEEE\/ACM ICSE. arxiv:1910 .10601. T. Durieux, J. F. Ferreira, R. Abreu, and P. Cruz. 2020. Empirical review of automated analysis tools on 47,587 ethereum smart contracts. In Proceedings of the IEEE\/ACM ICSE. arxiv:1910.10601."},{"key":"e_1_2_1_63_1","volume-title":"Proceedings of the EDCC. IEEE, 158\u2013163","author":"Ellul J.","unstructured":"J. Ellul and G. J. Pace . 2018. Runtime verification of ethereum smart contracts . In Proceedings of the EDCC. IEEE, 158\u2013163 . J. Ellul and G. J. Pace. 2018. Runtime verification of ethereum smart contracts. In Proceedings of the EDCC. IEEE, 158\u2013163."},{"key":"e_1_2_1_64_1","volume-title":"Slither: A static analysis framework for smart contracts. In Proceedings of the","author":"Feist J.","year":"2019","unstructured":"J. Feist , G. Greico , and A. Groce . 2019 . Slither: A static analysis framework for smart contracts. In Proceedings of the IEEE\/ACM WETSEB. IEEE Press , 8\u201315. J. Feist, G. Greico, and A. Groce. 2019. Slither: A static analysis framework for smart contracts. In Proceedings of the IEEE\/ACM WETSEB. IEEE Press, 8\u201315."},{"key":"e_1_2_1_65_1","unstructured":"Y. Feng E. Torlak and R. Bod\u00edk. 2019. Precise attack synthesis for smart contracts. arxiv:1902.06067.  Y. Feng E. Torlak and R. Bod\u00edk. 2019. Precise attack synthesis for smart contracts. arxiv:1902.06067."},{"key":"e_1_2_1_66_1","volume-title":"Proceedings of the ACM CCS. ACM, 2589\u20132591","author":"Torres C. Ferreira","unstructured":"C. Ferreira Torres , M. Baden , R. Norvill , and H. Jonker . 2019. \u00c6GIS: Smart shielding of smart contracts . In Proceedings of the ACM CCS. ACM, 2589\u20132591 . C. Ferreira Torres, M. Baden, R. Norvill, and H. Jonker. 2019. \u00c6GIS: Smart shielding of smart contracts. In Proceedings of the ACM CCS. ACM, 2589\u20132591."},{"key":"e_1_2_1_67_1","volume-title":"Proceedings of the ACSAC. ACM, 664\u2013676","author":"Torres C. Ferreira","unstructured":"C. Ferreira Torres , J. Sch\u00fctte , and R. State . 2018. Osiris: Hunting for integer bugs in ethereum smart contracts . In Proceedings of the ACSAC. ACM, 664\u2013676 . C. Ferreira Torres, J. Sch\u00fctte, and R. State. 2018. Osiris: Hunting for integer bugs in ethereum smart contracts. In Proceedings of the ACSAC. ACM, 664\u2013676."},{"key":"e_1_2_1_68_1","volume-title":"Proceedings of the ICBC","volume":"11521","author":"Fournier F.","unstructured":"F. Fournier and I. Skarbovsky . 2019. Enriching smart contracts with temporal aspects . In Proceedings of the ICBC , Vol. 11521 LNCS. Springer Verlag, 126\u2013141. F. Fournier and I. Skarbovsky. 2019. Enriching smart contracts with temporal aspects. In Proceedings of the ICBC, Vol. 11521 LNCS. Springer Verlag, 126\u2013141."},{"key":"e_1_2_1_69_1","volume-title":"ETHBMC: A bounded model checker for smart contracts. In Proceedings of the USENIX Security","author":"Frank J.","year":"2020","unstructured":"J. Frank , C. Aschermann , and T. Holz . 2020 . ETHBMC: A bounded model checker for smart contracts. In Proceedings of the USENIX Security . USENIX Association . J. Frank, C. Aschermann, and T. Holz. 2020. ETHBMC: A bounded model checker for smart contracts. In Proceedings of the USENIX Security. USENIX Association."},{"key":"e_1_2_1_70_1","volume-title":"Proceedings of the IEEE FAS-W. IEEE, 210\u2013215","author":"Frantz C. K.","unstructured":"C. K. Frantz and M. Nowostawski . 2016. From institutions to code: Towards automated generation of smart contracts . In Proceedings of the IEEE FAS-W. IEEE, 210\u2013215 . C. K. Frantz and M. Nowostawski. 2016. From institutions to code: Towards automated generation of smart contracts. In Proceedings of the IEEE FAS-W. IEEE, 210\u2013215."},{"key":"e_1_2_1_71_1","volume-title":"Proceedings of the the IEEE\/ACM ICSE-Companion. 23\u201326","author":"Gao J.","unstructured":"J. Gao , H. Liu , C. Liu , Q. Li , Z. Guan , and Z. Chen . 2019. EASYFLOW: Keep ethereum away from overflow . In Proceedings of the the IEEE\/ACM ICSE-Companion. 23\u201326 . J. Gao, H. Liu, C. Liu, Q. Li, Z. Guan, and Z. Chen. 2019. EASYFLOW: Keep ethereum away from overflow. In Proceedings of the the IEEE\/ACM ICSE-Companion. 23\u201326."},{"key":"e_1_2_1_72_1","unstructured":"T. Genet T. Jensen and J. Sauvage. 2020. Termination of Ethereum\u2019s Smart Contracts. Research Report. Univ Rennes Inria CNRS IRISA. Retrieved from https:\/\/hal.inria.fr\/hal-02555738.  T. Genet T. Jensen and J. Sauvage. 2020. Termination of Ethereum\u2019s Smart Contracts. Research Report. Univ Rennes Inria CNRS IRISA. Retrieved from https:\/\/hal.inria.fr\/hal-02555738."},{"key":"e_1_2_1_73_1","unstructured":"L. M. Goodman. 2014. Tezos \u2014 A Self-Amending Crypto-Ledger. White Paper. Retrieved from https:\/\/tezos.com\/static\/white_paper-2dc8c02267a8fb86bd67a108199441bf.pdf.  L. M. Goodman. 2014. Tezos \u2014 A Self-Amending Crypto-Ledger. White Paper. Retrieved from https:\/\/tezos.com\/static\/white_paper-2dc8c02267a8fb86bd67a108199441bf.pdf."},{"key":"e_1_2_1_74_1","volume-title":"Thou shalt is not you will. CoRR abs\/1404.1685","author":"Governatori G.","year":"2014","unstructured":"G. Governatori . 2014. Thou shalt is not you will. CoRR abs\/1404.1685 ( 2014 ). G. Governatori. 2014. Thou shalt is not you will. CoRR abs\/1404.1685 (2014)."},{"key":"e_1_2_1_75_1","doi-asserted-by":"crossref","unstructured":"G. Governatori F. Idelberger Z. Milosevic R. Riveret G. Sartor and X. Xu. 2018. On legal contracts imperative and declarative smart contracts and blockchain systems. Artif. Intell. Law 26 4 (01 Dec. 2018) 377\u2013409.  G. Governatori F. Idelberger Z. Milosevic R. Riveret G. Sartor and X. Xu. 2018. On legal contracts imperative and declarative smart contracts and blockchain systems. Artif. Intell. Law 26 4 (01 Dec. 2018) 377\u2013409.","DOI":"10.1007\/s10506-018-9223-3"},{"key":"e_1_2_1_76_1","volume-title":"Proceedings of the IEEE\/ACM ICSE. 1176\u20131186","author":"Grech N.","unstructured":"N. Grech , L. Brent , B. Scholz , and Y. Smaragdakis . 2019. Gigahorse: Thorough, declarative decompilation of smart contracts . In Proceedings of the IEEE\/ACM ICSE. 1176\u20131186 . N. Grech, L. Brent, B. Scholz, and Y. Smaragdakis. 2019. Gigahorse: Thorough, declarative decompilation of smart contracts. In Proceedings of the IEEE\/ACM ICSE. 1176\u20131186."},{"key":"e_1_2_1_77_1","volume-title":"Proceedings of the ACM OOPSLA.","author":"Grech N.","unstructured":"N. Grech , M. Kong , A. Jurisevic , L. Brent , B. Scholz , and Y. Smaragdakis . 2018. MadMax: Surviving out-of-gas conditions in ethereum smart contracts . In Proceedings of the ACM OOPSLA. N. Grech, M. Kong, A. Jurisevic, L. Brent, B. Scholz, and Y. Smaragdakis. 2018. MadMax: Surviving out-of-gas conditions in ethereum smart contracts. In Proceedings of the ACM OOPSLA."},{"key":"e_1_2_1_78_1","volume-title":"Proceedings of the POST. Springer, Cham, 243\u2013269","author":"Grishchenko I.","unstructured":"I. Grishchenko , M. Maffei , and C. Schneidewind . 2018. A semantic framework for the security analysis of ethereum smart contracts . In Proceedings of the POST. Springer, Cham, 243\u2013269 . I. Grishchenko, M. Maffei, and C. Schneidewind. 2018. A semantic framework for the security analysis of ethereum smart contracts. In Proceedings of the POST. Springer, Cham, 243\u2013269."},{"key":"e_1_2_1_79_1","doi-asserted-by":"crossref","unstructured":"A. Groce J. Feist G. Grieco and M. Colburn. 2019. What are the Actual Flaws in Important Smart Contracts (and How Can We Find Them)?arxiv:1911.07567.  A. Groce J. Feist G. Grieco and M. Colburn. 2019. What are the Actual Flaws in Important Smart Contracts (and How Can We Find Them)?arxiv:1911.07567.","DOI":"10.1007\/978-3-030-51280-4_34"},{"key":"e_1_2_1_80_1","volume-title":"Proceedings of the ACM POPL.","author":"Grossman S.","unstructured":"S. Grossman , I. Abraham , G. Golan-Gueta , Y. Michalevsky , N. Rinetzky , M. Sagiv , and Y. Zohar . 2017. Online detection of effectively callback free objects with applications to smart contracts . Proceedings of the ACM POPL. S. Grossman, I. Abraham, G. Golan-Gueta, Y. Michalevsky, N. Rinetzky, M. Sagiv, and Y. Zohar. 2017. Online detection of effectively callback free objects with applications to smart contracts. Proceedings of the ACM POPL."},{"key":"e_1_2_1_81_1","unstructured":"NCC Group. 2018. TOP 10 \u2014 Arithmetic Issues. Retrieved from https:\/\/www.dasp.co\/.  NCC Group. 2018. TOP 10 \u2014 Arithmetic Issues. Retrieved from https:\/\/www.dasp.co\/."},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00196791"},{"key":"e_1_2_1_83_1","unstructured":"\u00c1. Hajdu and D. Jovanovi\u0107. 2019. solc-verify: A modular verifier for solidity smart contracts. arxiv:1907.04262.  \u00c1. Hajdu and D. Jovanovi\u0107. 2019. solc-verify: A modular verifier for solidity smart contracts. arxiv:1907.04262."},{"key":"e_1_2_1_84_1","unstructured":"\u00c1. Hajdu D. Jovanovi\u0107 and G. Ciocarlie. 2020. Formal Specification and Verification of Solidity Contracts with Events. arxiv:2005.10382.  \u00c1. Hajdu D. Jovanovi\u0107 and G. Ciocarlie. 2020. Formal Specification and Verification of Solidity Contracts with Events. arxiv:2005.10382."},{"key":"e_1_2_1_85_1","unstructured":"D. Harz and W. Knottenbelt. 2018. Towards safer smart contracts: A survey of languages and verification methods. arxiv:1809.09805.  D. Harz and W. Knottenbelt. 2018. Towards safer smart contracts: A survey of languages and verification methods. arxiv:1809.09805."},{"key":"e_1_2_1_86_1","volume-title":"Proceedings of the ACM CCS. ACM, 531\u2013548","author":"He J.","unstructured":"J. He , M. Balunovic\u0300 , N. Ambroladze , P. Tsankov , and M. Vechev . 2019. Learning to fuzz from symbolic execution with application to smart contracts . In Proceedings of the ACM CCS. ACM, 531\u2013548 . J. He, M. Balunovic\u0300, N. Ambroladze, P. Tsankov, and M. Vechev. 2019. Learning to fuzz from symbolic execution with application to smart contracts. In Proceedings of the ACM CCS. ACM, 531\u2013548."},{"key":"e_1_2_1_87_1","unstructured":"N. He R. Zhang L. Wu H. Wang X. Luo Y. Guo T. Yu and X. Jiang. 2020. Security Analysis of EOSIO Smart Contracts. arxiv:2003.06568.  N. He R. Zhang L. Wu H. Wang X. Luo Y. Guo T. Yu and X. Jiang. 2020. Security Analysis of EOSIO Smart Contracts. arxiv:2003.06568."},{"key":"e_1_2_1_88_1","unstructured":"Y. Hirai. 2016. Formal Verification of Deed Contract in Ethereum Name Service. Retrieved from https:\/\/yoichihirai.com\/deed.pdf.  Y. Hirai. 2016. Formal Verification of Deed Contract in Ethereum Name Service. Retrieved from https:\/\/yoichihirai.com\/deed.pdf."},{"key":"e_1_2_1_89_1","volume-title":"Proceedings of the","author":"Hirai Y.","unstructured":"Y. Hirai . 2017. Defining the ethereum virtual machine for interactive theorem provers . In Proceedings of the FC. Springer , Cham , 520\u2013535. Y. Hirai. 2017. Defining the ethereum virtual machine for interactive theorem provers. In Proceedings of the FC. Springer, Cham, 520\u2013535."},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03427-6_29"},{"key":"e_1_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2946988"},{"key":"e_1_2_1_93_1","volume-title":"Proceedings of the IEEE\/ACM ICPC. 260\u2013270","author":"Huang Y.","unstructured":"Y. Huang , Q. Kong , N. Jia , X. Chen , and Z. Zheng . 2019. Recommending differentiated code to support smart contract update . In Proceedings of the IEEE\/ACM ICPC. 260\u2013270 . Y. Huang, Q. Kong, N. Jia, X. Chen, and Z. Zheng. 2019. Recommending differentiated code to support smart contract update. In Proceedings of the IEEE\/ACM ICPC. 260\u2013270."},{"key":"e_1_2_1_94_1","volume-title":"Proceedings of the ADVANCE. 1\u20138.","author":"Imeri A.","unstructured":"A. Imeri , N. Agoulmine , and D. Khadraoui . 2020. Smart contract modeling and verification techniques: A survey . In Proceedings of the ADVANCE. 1\u20138. A. Imeri, N. Agoulmine, and D. Khadraoui. 2020. Smart contract modeling and verification techniques: A survey. In Proceedings of the ADVANCE. 1\u20138."},{"key":"e_1_2_1_95_1","unstructured":"Runtime Verification Inc.2018. ERC20-K: Formal Executable Specification of ERC20. Retrieved from https:\/\/github.com\/runtimeverification\/erc20-semantics.  Runtime Verification Inc.2018. ERC20-K: Formal Executable Specification of ERC20. Retrieved from https:\/\/github.com\/runtimeverification\/erc20-semantics."},{"key":"e_1_2_1_96_1","volume-title":"Proceedings of the IEEE S&P. IEEE Computer Society, 1265\u20131282","author":"Jiao J.","unstructured":"J. Jiao , S. Kan , S.-W. Lin , D. San\u00e1n , Y. Liu , and J. Sun . 2020. Semantic understanding of smart contracts: Executable operational semantics of solidity . In Proceedings of the IEEE S&P. IEEE Computer Society, 1265\u20131282 . J. Jiao, S. Kan, S.-W. Lin, D. San\u00e1n, Y. Liu, and J. Sun. 2020. Semantic understanding of smart contracts: Executable operational semantics of solidity. In Proceedings of the IEEE S&P. IEEE Computer Society, 1265\u20131282."},{"key":"e_1_2_1_97_1","volume-title":"Proceedings of the NDSS.","author":"Kalra S.","unstructured":"S. Kalra , S. Goel , M. Dhawan , and S. Sharma . 2018. ZEUS: Analyzing safety of smart contracts . In Proceedings of the NDSS. S. Kalra, S. Goel, M. Dhawan, and S. Sharma. 2018. ZEUS: Analyzing safety of smart contracts. In Proceedings of the NDSS."},{"key":"e_1_2_1_98_1","volume-title":"Proceedings of the FM.","author":"Kasampalis T.","unstructured":"T. Kasampalis , D. Guth , B. Moore , T. F. Serbanuta , Y. Zhang , D. Filaretti , V. Serbanuta , R. Johnson , and G. Ro\u015fu . 2019. IELE: A rigorously designed language and tool ecosystem for the blockchain . In Proceedings of the FM. T. Kasampalis, D. Guth, B. Moore, T. F. Serbanuta, Y. Zhang, D. Filaretti, V. Serbanuta, R. Johnson, and G. Ro\u015fu. 2019. IELE: A rigorously designed language and tool ecosystem for the blockchain. In Proceedings of the FM."},{"key":"e_1_2_1_99_1","volume-title":"Proceedings of the ACM ISSTA. ACM, 363\u2013373","author":"Kolluri A.","unstructured":"A. Kolluri , I. Nikolic , I. Sergey , A. Hobor , and P. Saxena . 2019. Exploiting the laws of order in smart contracts . In Proceedings of the ACM ISSTA. ACM, 363\u2013373 . A. Kolluri, I. Nikolic, I. Sergey, A. Hobor, and P. Saxena. 2019. Exploiting the laws of order in smart contracts. In Proceedings of the ACM ISSTA. ACM, 363\u2013373."},{"key":"e_1_2_1_100_1","volume-title":"Proceedings of the ACM\/IEEE ASEW. 69\u201376","author":"Kongmanee J.","unstructured":"J. Kongmanee , P. Kijsanayothin , and R. Hewett . 2019. Securing smart contracts in blockchain . In Proceedings of the ACM\/IEEE ASEW. 69\u201376 . J. Kongmanee, P. Kijsanayothin, and R. Hewett. 2019. Securing smart contracts in blockchain. In Proceedings of the ACM\/IEEE ASEW. 69\u201376."},{"key":"e_1_2_1_101_1","volume-title":"Proceedings of the IEEE S&P. 839\u2013858","author":"Kosba A.","unstructured":"A. Kosba , A. Miller , E. Shi , Z. Wen , and C. Papamanthou . 2016. Hawk: The blockchain model of cryptography and privacy-preserving smart contracts . In Proceedings of the IEEE S&P. 839\u2013858 . A. Kosba, A. Miller, E. Shi, Z. Wen, and C. Papamanthou. 2016. Hawk: The blockchain model of cryptography and privacy-preserving smart contracts. In Proceedings of the IEEE S&P. 839\u2013858."},{"key":"e_1_2_1_102_1","volume-title":"Proceedings of the USENIX Security. ACM, 1317\u20131333","author":"Krupp J.","unstructured":"J. Krupp and C. Rossow . 2018. teEther: Gnawing at ethereum to automatically exploit smart contracts . In Proceedings of the USENIX Security. ACM, 1317\u20131333 . J. Krupp and C. Rossow. 2018. teEther: Gnawing at ethereum to automatically exploit smart contracts. In Proceedings of the USENIX Security. ACM, 1317\u20131333."},{"key":"e_1_2_1_103_1","unstructured":"A. Juels L. Breidenbach P. Daian and E. G. Sirer. 2017. An In-Depth Look at the Parity Multisig Bug. Retrieved from https:\/\/hackingdistributed.com\/2017\/07\/22\/deep-dive-parity-bug\/.  A. Juels L. Breidenbach P. Daian and E. G. Sirer. 2017. An In-Depth Look at the Parity Multisig Bug. Retrieved from https:\/\/hackingdistributed.com\/2017\/07\/22\/deep-dive-parity-bug\/."},{"key":"e_1_2_1_104_1","volume-title":"Proceedings of the ER. 323\u2013337","author":"Ladleif J.","unstructured":"J. Ladleif and M. Weske . 2019. A unifying model of legal smart contracts . In Proceedings of the ER. 323\u2013337 . J. Ladleif and M. Weske. 2019. A unifying model of legal smart contracts. In Proceedings of the ER. 323\u2013337."},{"key":"e_1_2_1_105_1","volume-title":"Marlowe: Implementing and analysing financial contracts on blockchain.","author":"Seijas P. Lamela","year":"2020","unstructured":"P. Lamela Seijas , A. Nemish , D. Smith , and S. Thompson . 2020 . Marlowe: Implementing and analysing financial contracts on blockchain. Retrieved from https:\/\/iohk.io\/en\/research\/library\/papers\/marloweimplementing-and-analysing-financial-contracts-on-blockchain\/. P. Lamela Seijas, A. Nemish, D. Smith, and S. Thompson. 2020. Marlowe: Implementing and analysing financial contracts on blockchain. Retrieved from https:\/\/iohk.io\/en\/research\/library\/papers\/marloweimplementing-and-analysing-financial-contracts-on-blockchain\/."},{"key":"e_1_2_1_106_1","doi-asserted-by":"crossref","unstructured":"C. Laneve C. S. Coen and A. Veschetti. 2019. On the Prediction of Smart Contracts\u2019 Behaviours. Springer International Publishing 397\u2013415.  C. Laneve C. S. Coen and A. Veschetti. 2019. On the Prediction of Smart Contracts\u2019 Behaviours. Springer International Publishing 397\u2013415.","DOI":"10.1007\/978-3-030-30985-5_23"},{"key":"e_1_2_1_107_1","volume-title":"Proceedings of the ACM PLDI. ACM, 438\u2013453","author":"Li A.","unstructured":"A. Li , J. A. Choi , and F. Long . 2020. Securing smart contract with runtime validation . In Proceedings of the ACM PLDI. ACM, 438\u2013453 . A. Li, J. A. Choi, and F. Long. 2020. Securing smart contract with runtime validation. In Proceedings of the ACM PLDI. ACM, 438\u2013453."},{"key":"e_1_2_1_108_1","unstructured":"A. Li and F. Long. 2018. Detecting standard violation errors in smart contracts. arxiv:1812.07702.  A. Li and F. Long. 2018. Detecting standard violation errors in smart contracts. arxiv:1812.07702."},{"key":"e_1_2_1_109_1","volume-title":"Proceedings of the ICFEM. Springer International Publishing, 121\u2013137","author":"Li X.","unstructured":"X. Li , Z. Shi , Q. Zhang , G. Wang , Y. Guan , and N. Han . 2019. Towards verifying ethereum smart contracts at intermediate language level . In Proceedings of the ICFEM. Springer International Publishing, 121\u2013137 . X. Li, Z. Shi, Q. Zhang, G. Wang, Y. Guan, and N. Han. 2019. Towards verifying ethereum smart contracts at intermediate language level. In Proceedings of the ICFEM. Springer International Publishing, 121\u2013137."},{"key":"e_1_2_1_110_1","volume-title":"Proceedings of the the BIGCOM. 74\u201378","author":"Li X.","unstructured":"X. Li , C. Su , Y. Xiong , W. Huang , and W. Wang . 2019. Formal verification of BNB smart contract . In Proceedings of the the BIGCOM. 74\u201378 . X. Li, C. Su, Y. Xiong, W. Huang, and W. Wang. 2019. Formal verification of BNB smart contract. In Proceedings of the the BIGCOM. 74\u201378."},{"key":"e_1_2_1_111_1","volume-title":"Proceedings of the IEEE\/ACM ICSE. ACM, 65\u201368","author":"Liu C.","unstructured":"C. Liu , H. Liu , Z. Cao , Z. Chen , B. Chen , and B. Roscoe . 2018. ReGuard: Finding reentrancy bugs in smart contracts . In Proceedings of the IEEE\/ACM ICSE. ACM, 65\u201368 . C. Liu, H. Liu, Z. Cao, Z. Chen, B. Chen, and B. Roscoe. 2018. ReGuard: Finding reentrancy bugs in smart contracts. In Proceedings of the IEEE\/ACM ICSE. ACM, 65\u201368."},{"key":"e_1_2_1_112_1","volume-title":"Proceedings of the ACM\/IEEE ASE. ACM, 814\u2013819","author":"Liu H.","unstructured":"H. Liu , C. Liu , W. Zhao , Y. Jiang , and J. Sun . 2018. S-gram: Towards semantic-aware security auditing for ethereum smart contracts . In Proceedings of the ACM\/IEEE ASE. ACM, 814\u2013819 . H. Liu, C. Liu, W. Zhao, Y. Jiang, and J. Sun. 2018. S-gram: Towards semantic-aware security auditing for ethereum smart contracts. In Proceedings of the ACM\/IEEE ASE. ACM, 814\u2013819."},{"key":"e_1_2_1_113_1","volume-title":"Proceedings of the ACM ESEC\/FSE.","author":"Liu Y.","unstructured":"Y. Liu , Y. Li , S.-W. Lin , and R. Zhao . 2020. Towards automated verification of smart contract fairness . In Proceedings of the ACM ESEC\/FSE. Y. Liu, Y. Li, S.-W. Lin, and R. Zhao. 2020. Towards automated verification of smart contract fairness. In Proceedings of the ACM ESEC\/FSE."},{"key":"e_1_2_1_114_1","volume-title":"Proceedings of the IEEE ISSRE.","author":"Liu Y.","unstructured":"Y. Liu , J. Sun , and J. S. Dong . 2011. PAT 3: An extensible architecture for building multi-domain model checkers . In Proceedings of the IEEE ISSRE. Y. Liu, J. Sun, and J. S. Dong. 2011. PAT 3: An extensible architecture for building multi-domain model checkers. In Proceedings of the IEEE ISSRE."},{"key":"e_1_2_1_115_1","volume-title":"Proceedings of the IEEE COMPSAC. IEEE, 555\u2013560","author":"Liu Z.","unstructured":"Z. Liu and J. Liu . 2019. Formal verification of blockchain smart contract based on colored petri net models . In Proceedings of the IEEE COMPSAC. IEEE, 555\u2013560 . Z. Liu and J. Liu. 2019. Formal verification of blockchain smart contract based on colored petri net models. In Proceedings of the IEEE COMPSAC. IEEE, 555\u2013560."},{"key":"e_1_2_1_116_1","volume-title":"Proceedings of the ACM CCS. ACM, 254\u2013269","author":"Luu L.","unstructured":"L. Luu , D.-H. Chu , H. Olickel , P. Saxena , and A. Hobor . 2016. Making smart contracts smarter . In Proceedings of the ACM CCS. ACM, 254\u2013269 . L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor. 2016. Making smart contracts smarter. In Proceedings of the ACM CCS. ACM, 254\u2013269."},{"key":"e_1_2_1_117_1","volume-title":"Proceedings of the IEEE SANER. 554\u2013558","author":"Ma F.","unstructured":"F. Ma , Y. Fu , M. Ren , M. Wang , Y. Jiang , K. Zhang , H. Li , and X. Shi . 2019. EVM*: From offline detection to online reinforcement for ethereum virtual machine . In Proceedings of the IEEE SANER. 554\u2013558 . F. Ma, Y. Fu, M. Ren, M. Wang, Y. Jiang, K. Zhang, H. Li, and X. Shi. 2019. EVM*: From offline detection to online reinforcement for ethereum virtual machine. In Proceedings of the IEEE SANER. 554\u2013558."},{"key":"e_1_2_1_118_1","volume-title":"Proceedings of the IEEE Blockchain. 556\u2013563","author":"Madl G.","unstructured":"G. Madl , L. Bathen , G. Flores , and D. Jadav . 2019. Formal verification of smart contracts using interface automata . In Proceedings of the IEEE Blockchain. 556\u2013563 . G. Madl, L. Bathen, G. Flores, and D. Jadav. 2019. Formal verification of smart contracts using interface automata. In Proceedings of the IEEE Blockchain. 556\u2013563."},{"key":"e_1_2_1_119_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2017.3571045"},{"key":"e_1_2_1_120_1","volume-title":"IOP Conf. Ser. Mater. Sci. Eng. 734 (Jan.","author":"Maksimov D. B.","year":"2020","unstructured":"D. B. Maksimov , I. A. Yakimov , and A. S. Kuznetsov . 2020. Statistical model checking for blockchain-based applications . IOP Conf. Ser. Mater. Sci. Eng. 734 (Jan. 2020 ), 012152. D. B. Maksimov, I. A. Yakimov, and A. S. Kuznetsov. 2020. Statistical model checking for blockchain-based applications. IOP Conf. Ser. Mater. Sci. Eng. 734 (Jan. 2020), 012152."},{"key":"e_1_2_1_121_1","doi-asserted-by":"crossref","unstructured":"A. Mavridou A. Laszka E. Stachtiari and A. Dubey. 2019. VeriSolid: Correct-by-design smart contracts for ethereum. arxiv:1901.01292.  A. Mavridou A. Laszka E. Stachtiari and A. Dubey. 2019. VeriSolid: Correct-by-design smart contracts for ethereum. arxiv:1901.01292.","DOI":"10.1007\/978-3-030-32101-7_27"},{"key":"e_1_2_1_122_1","volume-title":"Proceedings of the ISoLA","volume":"11247","author":"Miller A.","unstructured":"A. Miller , Z. Cai , and S. Jha . 2018. Smart contracts and opportunities for formal methods . In Proceedings of the ISoLA , Vol. 11247 LNCS. Springer Verlag, 280\u2013299. A. Miller, Z. Cai, and S. Jha. 2018. Smart contracts and opportunities for formal methods. In Proceedings of the ISoLA, Vol. 11247 LNCS. Springer Verlag, 280\u2013299."},{"key":"e_1_2_1_123_1","volume-title":"Proceedings of the IEEE SC2. 83\u201390","author":"Molina-Jimenez C.","unstructured":"C. Molina-Jimenez , I. Sfyrakis , E. Solaiman , I. Ng , M. Weng Wong , A. Chun , and J. Crowcroft . 2018. Implementation of smart contracts using hybrid architectures with on and off-blockchain components . In Proceedings of the IEEE SC2. 83\u201390 . C. Molina-Jimenez, I. Sfyrakis, E. Solaiman, I. Ng, M. Weng Wong, A. Chun, and J. Crowcroft. 2018. Implementation of smart contracts using hybrid architectures with on and off-blockchain components. In Proceedings of the IEEE SC2. 83\u201390."},{"key":"e_1_2_1_124_1","volume-title":"Proceedings of the ACM\/IEEE ASE. 1186\u20131189","author":"Mossberg M.","unstructured":"M. Mossberg , F. Manzano , E. Hennenfent , A. Groce , G. Grieco , J. Feist , T. Brunson , and A. Dinaburg . 2019. Manticore: A user-friendly symbolic execution framework for binaries and smart contracts . In Proceedings of the ACM\/IEEE ASE. 1186\u20131189 . M. Mossberg, F. Manzano, E. Hennenfent, A. Groce, G. Grieco, J. Feist, T. Brunson, and A. Dinaburg. 2019. Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. In Proceedings of the ACM\/IEEE ASE. 1186\u20131189."},{"key":"e_1_2_1_126_1","volume-title":"Retrieved","author":"Nakamoto S.","year":"2008","unstructured":"S. Nakamoto . 2008 . Bitcoin: A Peer-to-Peer Electronic Cash System . Retrieved July 14, (2020) from https:\/\/bitcoin.org\/bitcoin.pdf\/. (2008). S. Nakamoto. 2008. Bitcoin: A Peer-to-Peer Electronic Cash System. Retrieved July 14, (2020) from https:\/\/bitcoin.org\/bitcoin.pdf\/. (2008)."},{"key":"e_1_2_1_127_1","unstructured":"Z. Nehai and F. Bobot. 2019. Deductive proof of ethereum smart contracts using why3. arxiv:1904.11281.  Z. Nehai and F. Bobot. 2019. Deductive proof of ethereum smart contracts using why3. arxiv:1904.11281."},{"key":"e_1_2_1_128_1","volume-title":"Proceedings of the IEEE iThings\/GreenCom\/CPSCom\/SmartData. IEEE, 980\u2013987","author":"Nehai Z.","unstructured":"Z. Nehai , P. Piriou , and F. Daumas . 2018. Model-checking of smart contracts . In Proceedings of the IEEE iThings\/GreenCom\/CPSCom\/SmartData. IEEE, 980\u2013987 . Z. Nehai, P. Piriou, and F. Daumas. 2018. Model-checking of smart contracts. In Proceedings of the IEEE iThings\/GreenCom\/CPSCom\/SmartData. IEEE, 980\u2013987."},{"key":"e_1_2_1_129_1","doi-asserted-by":"crossref","unstructured":"K. Nelaturu A. Mavridou A. Veneris and A. Laszka. 2020. Verified development and deployment of multiple interacting smart contracts with verisolid. Retrieved from http:\/\/www.eecg.utoronto.ca\/ veneris\/20ICBC.pdf.  K. Nelaturu A. Mavridou A. Veneris and A. Laszka. 2020. Verified development and deployment of multiple interacting smart contracts with verisolid. Retrieved from http:\/\/www.eecg.utoronto.ca\/ veneris\/20ICBC.pdf.","DOI":"10.1109\/ICBC48266.2020.9169428"},{"key":"e_1_2_1_130_1","unstructured":"J. B. Nielsen and B. Spitters. 2019. Smart Contract Interactions in Coq. arxiv:1911.04732.  J. B. Nielsen and B. Spitters. 2019. Smart Contract Interactions in Coq. arxiv:1911.04732."},{"key":"e_1_2_1_131_1","volume-title":"Proceedings of the ACSAC.","author":"Nikoli\u0107 I.","unstructured":"I. Nikoli\u0107 , A. Kolluri , I. Sergey , P. Saxena , and A. Hobor . 2018. Finding the greedy, prodigal, and suicidal contracts at scale . Proceedings of the ACSAC. I. Nikoli\u0107, A. Kolluri, I. Sergey, P. Saxena, and A. Hobor. 2018. Finding the greedy, prodigal, and suicidal contracts at scale. Proceedings of the ACSAC."},{"key":"e_1_2_1_132_1","doi-asserted-by":"publisher","DOI":"10.1145\/3139337.3139340"},{"key":"e_1_2_1_133_1","unstructured":"OpenZeppelin. 2020. SafeMath Library. Retrieved from https:\/\/github.com\/OpenZeppelin\/openzeppelin-contracts\/blob\/master\/contracts\/math\/SafeMath.sol.  OpenZeppelin. 2020. SafeMath Library. Retrieved from https:\/\/github.com\/OpenZeppelin\/openzeppelin-contracts\/blob\/master\/contracts\/math\/SafeMath.sol."},{"key":"e_1_2_1_134_1","volume-title":"Proceedings of the ICBC","volume":"10974","author":"Parizi R. M.","unstructured":"R. M. Parizi , A. Singh , and A. Dehghantanha . 2018. Smart contract programming languages on blockchains: An empirical evaluation of usability and security . In Proceedings of the ICBC , Vol. 10974 LNCS. Springer Verlag, 75\u201391. R. M. Parizi, A. Singh, and A. Dehghantanha. 2018. Smart contract programming languages on blockchains: An empirical evaluation of usability and security. In Proceedings of the ICBC, Vol. 10974 LNCS. Springer Verlag, 75\u201391."},{"key":"e_1_2_1_135_1","volume-title":"Proceedings of the ACM ESEC\/FSE. ACM, 912\u2013915","author":"Park D.","unstructured":"D. Park , Y. Zhang , M. Saxena , P. Daian , and G. Ro\u015fu . 2018. A formal verification tool for ethereum VM bytecode . In Proceedings of the ACM ESEC\/FSE. ACM, 912\u2013915 . D. Park, Y. Zhang, M. Saxena, P. Daian, and G. Ro\u015fu. 2018. A formal verification tool for ethereum VM bytecode. In Proceedings of the ACM ESEC\/FSE. ACM, 912\u2013915."},{"key":"e_1_2_1_136_1","unstructured":"D. Perez and B. Livshits. 2019. Smart contract vulnerabilities: Does anyone care?arxiv:1902.06710.  D. Perez and B. Livshits. 2019. Smart contract vulnerabilities: Does anyone care?arxiv:1902.06710."},{"key":"e_1_2_1_137_1","volume-title":"Proceedings of the IEEE S&P. IEEE Computer Society, 414\u2013430","author":"Permenev A.","unstructured":"A. Permenev , D. Dimitrov , P. Tsankov , D. Drachsler-Cohen , and M. Vechev . 2020. VerX: Safety verification of smart contracts . In Proceedings of the IEEE S&P. IEEE Computer Society, 414\u2013430 . A. Permenev, D. Dimitrov, P. Tsankov, D. Drachsler-Cohen, and M. Vechev. 2020. VerX: Safety verification of smart contracts. In Proceedings of the IEEE S&P. IEEE Computer Society, 414\u2013430."},{"key":"e_1_2_1_138_1","unstructured":"S. Popejoy. 2017. The Pact Smart-Contract Language. Retrieved from https:\/\/www.kadena.io\/whitepapers.  S. Popejoy. 2017. The Pact Smart-Contract Language. Retrieved from https:\/\/www.kadena.io\/whitepapers."},{"key":"e_1_2_1_139_1","unstructured":"P. Praitheeshan L. Pan J. Yu J. Liu and R. Doss. 2019. Security analysis methods on ethereum smart contract vulnerabilities: A survey. arxiv:1908.08605.  P. Praitheeshan L. Pan J. Yu J. Liu and R. Doss. 2019. Security analysis methods on ethereum smart contract vulnerabilities: A survey. arxiv:1908.08605."},{"key":"e_1_2_1_140_1","volume-title":"Proceedings of the IFIP NTMS. 1\u20136.","author":"Prechtel D.","unstructured":"D. Prechtel , T. Gro\u00df , and T. M\u00fcller . 2019. Evaluating spread of \u201cgasless send\u201d in ethereum smart contracts . In Proceedings of the IFIP NTMS. 1\u20136. D. Prechtel, T. Gro\u00df, and T. M\u00fcller. 2019. Evaluating spread of \u201cgasless send\u201d in ethereum smart contracts. In Proceedings of the IFIP NTMS. 1\u20136."},{"key":"e_1_2_1_141_1","volume-title":"Proceedings of the SmartBlock","volume":"11373","author":"Qu M.","unstructured":"M. Qu , X. Huang , X. Chen , Y. Wang , X. Ma , and D. Liu . 2018. Formal verification of smart contracts from the perspective of concurrency . In Proceedings of the SmartBlock , Vol. 11373 LNCS. Springer Verlag, 32\u201343. M. Qu, X. Huang, X. Chen, Y. Wang, X. Ma, and D. Liu. 2018. Formal verification of smart contracts from the perspective of concurrency. In Proceedings of the SmartBlock, Vol. 11373 LNCS. Springer Verlag, 32\u201343."},{"key":"e_1_2_1_142_1","unstructured":"RChain. 2018. Contract Design \u2014 RChain Architecture 0.9.0 documentation. Retrieved from https:\/\/architecture-docs.readthedocs.io\/contracts\/contract-design.html.  RChain. 2018. Contract Design \u2014 RChain Architecture 0.9.0 documentation. Retrieved from https:\/\/architecture-docs.readthedocs.io\/contracts\/contract-design.html."},{"key":"e_1_2_1_143_1","unstructured":"J. S. Reis P. Crocker and S. M. de Sousa. 2020. Tezla an Intermediate Representation for Static Analysis of Michelson Smart Contracts. arxiv:2005.11839.  J. S. Reis P. Crocker and S. M. de Sousa. 2020. Tezla an Intermediate Representation for Static Analysis of Michelson Smart Contracts. arxiv:2005.11839."},{"key":"e_1_2_1_144_1","volume-title":"Theorem Proving for Verification","author":"Rushby J.","unstructured":"J. Rushby . 2001. Theorem Proving for Verification . Springer Berlin , 39\u201357. J. Rushby. 2001. Theorem Proving for Verification. Springer Berlin, 39\u201357."},{"key":"e_1_2_1_145_1","volume-title":"Proceedings of the IEEE IWBOSE. 22\u201329","author":"Samreen N. F.","unstructured":"N. F. Samreen and M. H. Alalfi . 2020. Reentrancy vulnerability identification in ethereum smart contracts . In Proceedings of the IEEE IWBOSE. 22\u201329 . N. F. Samreen and M. H. Alalfi. 2020. Reentrancy vulnerability identification in ethereum smart contracts. In Proceedings of the IEEE IWBOSE. 22\u201329."},{"key":"e_1_2_1_146_1","volume-title":"Raziel: Private and verifiable smart contracts on blockchains. CoRR abs\/1807.09484","author":"S\u00e1nchez D. C.","year":"2018","unstructured":"D. C. S\u00e1nchez . 2018. Raziel: Private and verifiable smart contracts on blockchains. CoRR abs\/1807.09484 ( 2018 ). D. C. S\u00e1nchez. 2018. Raziel: Private and verifiable smart contracts on blockchains. CoRR abs\/1807.09484 (2018)."},{"key":"e_1_2_1_147_1","volume-title":"Proceedings of the IEEE iThings\/GreenCom\/CPSCom\/SmartData. 945\u2013954","author":"Sato N.","unstructured":"N. Sato , T. Tateishi , and S. Amano . 2018. Formal requirement enforcement on smart contracts based on linear dynamic logic . In Proceedings of the IEEE iThings\/GreenCom\/CPSCom\/SmartData. 945\u2013954 . N. Sato, T. Tateishi, and S. Amano. 2018. Formal requirement enforcement on smart contracts based on linear dynamic logic. In Proceedings of the IEEE iThings\/GreenCom\/CPSCom\/SmartData. 945\u2013954."},{"key":"e_1_2_1_148_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2020.2970495"},{"key":"e_1_2_1_149_1","doi-asserted-by":"crossref","unstructured":"C. Schneidewind I. Grishchenko M. Scherer and M. Maffei. 2020. eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. arxiv:2005.06227.  C. Schneidewind I. Grishchenko M. Scherer and M. Maffei. 2020. eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. arxiv:2005.06227.","DOI":"10.1145\/3372297.3417250"},{"key":"e_1_2_1_150_1","volume-title":"Proceedings of the ACM Programming Companion. ACM, 218\u2013219","author":"Schrans F.","unstructured":"F. Schrans , S. Eisenbach , and S. Drossopoulou . 2018. Writing safe smart contracts in Flint . In Proceedings of the ACM Programming Companion. ACM, 218\u2013219 . F. Schrans, S. Eisenbach, and S. Drossopoulou. 2018. Writing safe smart contracts in Flint. In Proceedings of the ACM Programming Companion. ACM, 218\u2013219."},{"key":"e_1_2_1_151_1","volume-title":"Proceedings of the FC","volume":"10323","author":"Sergey I.","unstructured":"I. Sergey and A. Hobor . 2017. A concurrent perspective on smart contracts . In Proceedings of the FC , Vol. 10323 LNCS. Springer Verlag, 478\u2013493. I. Sergey and A. Hobor. 2017. A concurrent perspective on smart contracts. In Proceedings of the FC, Vol. 10323 LNCS. Springer Verlag, 478\u2013493."},{"key":"e_1_2_1_152_1","volume-title":"Proceedings of the ISoLA. Springer, Cham, 323\u2013338","author":"Sergey I.","unstructured":"I. Sergey , A. Kumar , and A. Hobor . 2018. Temporal properties of smart contracts . In Proceedings of the ISoLA. Springer, Cham, 323\u2013338 . I. Sergey, A. Kumar, and A. Hobor. 2018. Temporal properties of smart contracts. In Proceedings of the ISoLA. Springer, Cham, 323\u2013338."},{"key":"e_1_2_1_153_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360611"},{"key":"e_1_2_1_154_1","unstructured":"E. Shishkin. 2018. Debugging smart contract\u2019s business logic using symbolic model-checking. arxiv:1812.00619.  E. Shishkin. 2018. Debugging smart contract\u2019s business logic using symbolic model-checking. arxiv:1812.00619."},{"key":"e_1_2_1_155_1","unstructured":"D. Siegel. 2016. Understanding The DAO Attack \u2014 CoinDesk. Retrieved from https:\/\/www.coindesk.com\/understanding-dao-hack-journalists.  D. Siegel. 2016. Understanding The DAO Attack \u2014 CoinDesk. Retrieved from https:\/\/www.coindesk.com\/understanding-dao-hack-journalists."},{"key":"e_1_2_1_156_1","doi-asserted-by":"crossref","unstructured":"A. Singh R. Parizi Q. Zhang K.-K. R. Choo and A. Dehghantanha. 2019. Blockchain smart contracts formalization: Approaches and challenges to address vulnerabilities. Comput. Secur. 88 (10 2019) 101654.  A. Singh R. Parizi Q. Zhang K.-K. R. Choo and A. Dehghantanha. 2019. Blockchain smart contracts formalization: Approaches and challenges to address vulnerabilities. Comput. Secur. 88 (10 2019) 101654.","DOI":"10.1016\/j.cose.2019.101654"},{"key":"e_1_2_1_157_1","volume-title":"Proceedings of the IEEE S&P. IEEE Computer Society, 825\u2013841","author":"So S.","unstructured":"S. So , M. Lee , J. Park , H. Lee , and H. Oh . 2020. VeriSmart: A highly precise safety verifier for ethereum smart contracts . In Proceedings of the IEEE S&P. IEEE Computer Society, 825\u2013841 . S. So, M. Lee, J. Park, H. Lee, and H. Oh. 2020. VeriSmart: A highly precise safety verifier for ethereum smart contracts. In Proceedings of the IEEE S&P. IEEE Computer Society, 825\u2013841."},{"key":"e_1_2_1_158_1","volume-title":"Proceedings of the FC, Matthew Bernhard, Andrea Bracciali","author":"Spoto F.","unstructured":"F. Spoto . 2020. Enforcing determinism of Java smart contracts . In Proceedings of the FC, Matthew Bernhard, Andrea Bracciali , L. Jean Camp, Shin\u2019ichiro Matsuo, Alana Maurushat, Peter B. R\u00f8nne, and Massimiliano Sala (Eds.). Springer International Publishing , Cham , 568\u2013583. F. Spoto. 2020. Enforcing determinism of Java smart contracts. In Proceedings of the FC, Matthew Bernhard, Andrea Bracciali, L. Jean Camp, Shin\u2019ichiro Matsuo, Alana Maurushat, Peter B. R\u00f8nne, and Massimiliano Sala (Eds.). Springer International Publishing, Cham, 568\u2013583."},{"key":"e_1_2_1_159_1","volume-title":"Proceedings of the ACM CCS. ACM, 1759\u20131776","author":"Steffen S.","unstructured":"S. Steffen , B. Bichsel , M. Gersbach , N. Melchior , P. Tsankov , and M. Vechev . 2019. zkay: Specifying and enforcing data privacy in smart contracts . In Proceedings of the ACM CCS. ACM, 1759\u20131776 . S. Steffen, B. Bichsel, M. Gersbach, N. Melchior, P. Tsankov, and M. Vechev. 2019. zkay: Specifying and enforcing data privacy in smart contracts. In Proceedings of the ACM CCS. ACM, 1759\u20131776."},{"key":"e_1_2_1_160_1","volume-title":"Proceedings of the ISoLA. Springer Berlin.","author":"Sun J.","unstructured":"J. Sun , Y. Liu , and J. S. Dong . 2008. Model checking CSP revisited: Introducing a process analysis toolkit . In Proceedings of the ISoLA. Springer Berlin. J. Sun, Y. Liu, and J. S. Dong. 2008. Model checking CSP revisited: Introducing a process analysis toolkit. In Proceedings of the ISoLA. Springer Berlin."},{"key":"e_1_2_1_161_1","doi-asserted-by":"publisher","DOI":"10.3390\/electronics9020255"},{"key":"e_1_2_1_162_1","unstructured":"D. Suvorov and V. Ulyantsev. 2019. Smart contract design meets state machine synthesis: Case studies. arxiv:1906.02906.  D. Suvorov and V. Ulyantsev. 2019. Smart contract design meets state machine synthesis: Case studies. arxiv:1906.02906."},{"key":"e_1_2_1_163_1","doi-asserted-by":"publisher","DOI":"10.5210\/fm.v2i9.548"},{"key":"e_1_2_1_164_1","unstructured":"Parity Technologies. 2017. A Postmortem on the Parity Multi-Sig Library Self-Destruct \u2014 Parity Technologies. Retrieved from https:\/\/www.parity.io\/a-postmortem-on-the-parity-multi-sig-library-self-destruct\/.  Parity Technologies. 2017. A Postmortem on the Parity Multi-Sig Library Self-Destruct \u2014 Parity Technologies. Retrieved from https:\/\/www.parity.io\/a-postmortem-on-the-parity-multi-sig-library-self-destruct\/."},{"key":"e_1_2_1_165_1","volume-title":"Proceedings of the IEEE\/ACM WETSEB. 9\u201316","author":"Tikhomirov S.","unstructured":"S. Tikhomirov , E. Voskresenskaya , I. Ivanitskiy , R. Takhaviev , E. Marchenko , and Y. Alexandrov . 2018. SmartCheck: Static analysis of ethereum smart contracts . In Proceedings of the IEEE\/ACM WETSEB. 9\u201316 . S. Tikhomirov, E. Voskresenskaya, I. Ivanitskiy, R. Takhaviev, E. Marchenko, and Y. Alexandrov. 2018. SmartCheck: Static analysis of ethereum smart contracts. In Proceedings of the IEEE\/ACM WETSEB. 9\u201316."},{"key":"e_1_2_1_166_1","doi-asserted-by":"crossref","unstructured":"P. Tolmach Y. Li S.-W. Lin and Y. Liu. 2021. Formal Analysis of Composable DeFi Protocols. arxiv:2103.00540.  P. Tolmach Y. Li S.-W. Lin and Y. Liu. 2021. Formal Analysis of Composable DeFi Protocols. arxiv:2103.00540.","DOI":"10.1007\/978-3-662-63958-0_13"},{"key":"e_1_2_1_167_1","volume-title":"Proceedings of the USENIX Security. USENIX Association, 1591\u20131607","author":"Torres C. Ferreira","unstructured":"C. Ferreira Torres , M. Steichen , and R. State . 2019. The art of the scam: Demystifying honeypots in ethereum smart contracts . In Proceedings of the USENIX Security. USENIX Association, 1591\u20131607 . C. Ferreira Torres, M. Steichen, and R. State. 2019. The art of the scam: Demystifying honeypots in ethereum smart contracts. In Proceedings of the USENIX Security. USENIX Association, 1591\u20131607."},{"key":"e_1_2_1_168_1","volume-title":"Proceedings of the ACM CCS. ACM, 67\u201382","author":"Tsankov P.","unstructured":"P. Tsankov , A. Dan , D. Drachsler-Cohen , A. Gervais , F. B\u00fcnzli , and M. Vechev . 2018. Securify: Practical security analysis of smart contracts . In Proceedings of the ACM CCS. ACM, 67\u201382 . P. Tsankov, A. Dan, D. Drachsler-Cohen, A. Gervais, F. B\u00fcnzli, and M. Vechev. 2018. Securify: Practical security analysis of smart contracts. In Proceedings of the ACM CCS. ACM, 67\u201382."},{"key":"e_1_2_1_169_1","doi-asserted-by":"publisher","DOI":"10.1109\/BLOC.2019.8751250"},{"key":"e_1_2_1_170_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2020.110647"},{"key":"e_1_2_1_171_1","unstructured":"F. Vogelsteller and V. Buterin. 2015. ERC-20 Token Standard. Retrieved from https:\/\/eips.ethereum.org\/EIPS\/eip-20.  F. Vogelsteller and V. Buterin. 2015. ERC-20 Token Standard. Retrieved from https:\/\/eips.ethereum.org\/EIPS\/eip-20."},{"key":"e_1_2_1_172_1","unstructured":"H. Wang Y. Li S.-W. Lin C. Artho L. Ma and Y. Liu. 2019. Oracle-Supported Dynamic Exploit Generation for Smart Contracts. arxiv:1909.06605.  H. Wang Y. Li S.-W. Lin C. Artho L. Ma and Y. Liu. 2019. Oracle-Supported Dynamic Exploit Generation for Smart Contracts. arxiv:1909.06605."},{"key":"e_1_2_1_173_1","volume-title":"VULTRON: Catching vulnerable smart contracts once and for all. In Proceedings of the","author":"Wang H.","year":"2019","unstructured":"H. Wang , Y. Li , S.-W. Lin , L. Ma , and Y. Liu . 2019 . VULTRON: Catching vulnerable smart contracts once and for all. In Proceedings of the IEEE\/ACM ICSE. IEEE Press , 1\u20134. H. Wang, Y. Li, S.-W. Lin, L. Ma, and Y. Liu. 2019. VULTRON: Catching vulnerable smart contracts once and for all. In Proceedings of the IEEE\/ACM ICSE. IEEE Press, 1\u20134."},{"key":"e_1_2_1_174_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSMC.2019.2895123"},{"key":"e_1_2_1_175_1","volume-title":"Proceedings of the ACM OOPSLA.","author":"Wang S.","unstructured":"S. Wang , C. Zhang , and Z. Su . 2019. Detecting nondeterministic payment bugs in ethereum smart contracts . Proceedings of the ACM OOPSLA. S. Wang, C. Zhang, and Z. Su. 2019. Detecting nondeterministic payment bugs in ethereum smart contracts. Proceedings of the ACM OOPSLA."},{"key":"e_1_2_1_176_1","doi-asserted-by":"crossref","unstructured":"Y. Wang S. Lahiri S. Chen R. Pan I. Dillig C. Born and I. Naseer. 2019. Formal Specification and Verification of Smart Contracts for Azure Blockchain. Retrieved from https:\/\/www.microsoft.com\/en-us\/research\/publication\/formal-specification-and-verification-of-smart-contracts-for-azure-blockchain\/.  Y. Wang S. Lahiri S. Chen R. Pan I. Dillig C. Born and I. Naseer. 2019. Formal Specification and Verification of Smart Contracts for Azure Blockchain. Retrieved from https:\/\/www.microsoft.com\/en-us\/research\/publication\/formal-specification-and-verification-of-smart-contracts-for-azure-blockchain\/.","DOI":"10.1007\/978-3-030-41600-3_7"},{"key":"e_1_2_1_177_1","volume-title":"Annotary: A concolic execution system for developing secure smart contracts. In Proceedings of the","author":"Weiss K.","year":"2019","unstructured":"K. Weiss and J. Sch\u00fctte . 2019 . Annotary: A concolic execution system for developing secure smart contracts. In Proceedings of the ESORICS. Springer International Publishing , 747\u2013766. K. Weiss and J. Sch\u00fctte. 2019. Annotary: A concolic execution system for developing secure smart contracts. In Proceedings of the ESORICS. Springer International Publishing, 747\u2013766."},{"key":"e_1_2_1_178_1","volume-title":"Proceedings of the IEEE iThings\/GreenCom\/CPSCom\/SmartData. IEEE, 1513\u20131520","author":"Wohrer M.","unstructured":"M. Wohrer and U. Zdun . 2018. Design patterns for smart contracts in the ethereum ecosystem . In Proceedings of the IEEE iThings\/GreenCom\/CPSCom\/SmartData. IEEE, 1513\u20131520 . M. Wohrer and U. Zdun. 2018. Design patterns for smart contracts in the ethereum ecosystem. In Proceedings of the IEEE iThings\/GreenCom\/CPSCom\/SmartData. IEEE, 1513\u20131520."},{"key":"e_1_2_1_179_1","first-page":"1","article-title":"Ethereum: A secure decentralised generalised transaction ledger","volume":"151","author":"Wood G.","year":"2014","unstructured":"G. Wood . 2014 . Ethereum: A secure decentralised generalised transaction ledger . Ether. Proj. Yell. Paper 151 (2014), 1 \u2013 32 . G. Wood. 2014. Ethereum: A secure decentralised generalised transaction ledger. Ether. Proj. Yell. Paper 151 (2014), 1\u201332.","journal-title":"Ether. Proj. Yell. Paper"},{"key":"e_1_2_1_180_1","unstructured":"W. Xu and G. A. Fink. 2019. Building Executable Secure Design Models for Smart Contracts with Formal Methods. arxiv:1912.04051.  W. Xu and G. A. Fink. 2019. Building Executable Secure Design Models for Smart Contracts with Formal Methods. arxiv:1912.04051."},{"key":"e_1_2_1_181_1","volume-title":"Proceedings of the ACM EuroPLoP. ACM, ACM.","author":"Xu X.","unstructured":"X. Xu , C. Pautasso , L. Zhu , Q. Lu , and I. Weber . 2018. A pattern collection for blockchain-based applications . In Proceedings of the ACM EuroPLoP. ACM, ACM. X. Xu, C. Pautasso, L. Zhu, Q. Lu, and I. Weber. 2018. A pattern collection for blockchain-based applications. In Proceedings of the ACM EuroPLoP. ACM, ACM."},{"key":"e_1_2_1_182_1","volume-title":"Proceedings of the IEEE IWBOSE. 1\u201310","author":"Yamashita K.","unstructured":"K. Yamashita , Y. Nomura , E. Zhou , B. Pi , and S. Jun . 2019. Potential risks of hyperledger fabric smart contracts . In Proceedings of the IEEE IWBOSE. 1\u201310 . K. Yamashita, Y. Nomura, E. Zhou, B. Pi, and S. Jun. 2019. Potential risks of hyperledger fabric smart contracts. In Proceedings of the IEEE IWBOSE. 1\u201310."},{"key":"e_1_2_1_183_1","volume-title":"Lolisa: Formal syntax and semantics for a subset of the solidity programming language. CoRR abs\/1803.09885","author":"Yang Z.","year":"2018","unstructured":"Z. Yang and H. Lei . 2018 . Lolisa: Formal syntax and semantics for a subset of the solidity programming language. CoRR abs\/1803.09885 (2018). Z. Yang and H. Lei. 2018. Lolisa: Formal syntax and semantics for a subset of the solidity programming language. CoRR abs\/1803.09885 (2018)."},{"key":"e_1_2_1_184_1","unstructured":"Z. Yang H. Lei and W. Qian. 2019. A hybrid formal verification system in Coq for ensuring the reliability and security of ethereum-based service smart contracts. CoRR abs\/1902.08726 (2019).  Z. Yang H. Lei and W. Qian. 2019. A hybrid formal verification system in Coq for ensuring the reliability and security of ethereum-based service smart contracts. CoRR abs\/1902.08726 (2019)."},{"key":"e_1_2_1_185_1","unstructured":"X. L. Yu O. Al-Bataineh D. Lo and A. Roychoudhury. 2019. Smart Contract Repair. arxiv:1912.05823.  X. L. Yu O. Al-Bataineh D. Lo and A. Roychoudhury. 2019. Smart Contract Repair. arxiv:1912.05823."},{"key":"e_1_2_1_186_1","volume-title":"Proceedings of the ACM CCS. ACM, 270\u2013282","author":"Zhang F.","unstructured":"F. Zhang , E. Cecchetti , K. Croman , A. Juels , and E. Shi . 2016. Town Crier: An authenticated data feed for smart contracts . In Proceedings of the ACM CCS. ACM, 270\u2013282 . F. Zhang, E. Cecchetti, K. Croman, A. Juels, and E. Shi. 2016. Town Crier: An authenticated data feed for smart contracts. In Proceedings of the ACM CCS. ACM, 270\u2013282."},{"key":"e_1_2_1_187_1","volume-title":"Proceedings of the COORDINATION. Springer International Publishing, 341\u2013349","author":"Zhang X.","unstructured":"X. Zhang , Y. Li , and M. Sun . 2020. Towards a formally verified EVM in production environment . In Proceedings of the COORDINATION. Springer International Publishing, 341\u2013349 . X. Zhang, Y. Li, and M. Sun. 2020. Towards a formally verified EVM in production environment. In Proceedings of the COORDINATION. Springer International Publishing, 341\u2013349."},{"key":"e_1_2_1_188_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2019.12.019"},{"key":"e_1_2_1_189_1","volume-title":"Proceedings of the IFIP NTMS. 1\u20135.","author":"Zhou E.","unstructured":"E. Zhou , S. Hua , B. Pi , J. Sun , Y. Nomura , K. Yamashita , and H. Kurihara . 2018. Security assurance for smart contract . In Proceedings of the IFIP NTMS. 1\u20135. E. Zhou, S. Hua, B. Pi, J. Sun, Y. Nomura, K. Yamashita, and H. Kurihara. 2018. Security assurance for smart contract. In Proceedings of the IFIP NTMS. 1\u20135."},{"key":"e_1_2_1_190_1","unstructured":"J. Zhu K. Hu M. Filali J.-P. Bodeveix and J.-P. Talpin. 2020. Formal Verification of Solidity contracts in Event-B. arxiv:2005.01261.  J. Zhu K. Hu M. Filali J.-P. Bodeveix and J.-P. Talpin. 2020. Formal Verification of Solidity contracts in Event-B. arxiv:2005.01261."},{"key":"e_1_2_1_191_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2942301"},{"key":"e_1_2_1_192_1","doi-asserted-by":"crossref","unstructured":"N. Zupan P. Kasinathan J. Cuellar and M. Sauer. 2020. Secure Smart Contract Generation Based on Petri Nets. Springer Singapore 73\u201398.  N. Zupan P. Kasinathan J. Cuellar and M. Sauer. 2020. Secure Smart Contract Generation Based on Petri Nets. Springer Singapore 73\u201398.","DOI":"10.1007\/978-981-15-1137-0_4"}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3464421","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3464421","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:17:10Z","timestamp":1750191430000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3464421"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,18]]},"references-count":191,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2022,9,30]]}},"alternative-id":["10.1145\/3464421"],"URL":"https:\/\/doi.org\/10.1145\/3464421","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,7,18]]},"assertion":[{"value":"2020-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-07-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}