{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:25:37Z","timestamp":1779074737270,"version":"3.51.4"},"reference-count":102,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"<jats:p>SMT-based verification of low-level code requires modeling and reasoning about memory operations. Prior work has shown that optimizing memory representations is beneficial for scaling verification\u2014pointer analysis, for example can be used to split memory into disjoint regions leading to faster SMT solving. However, these techniques are mostly designed for C and C++ programs with explicit operations for memory allocation which are not present in all languages. For instance, on the Ethereum virtual machine, memory is simply a monolithic array of bytes which can be freely accessed by Ethereum bytecode, and there is no allocation primitive.<\/jats:p>\n                  <jats:p>In this paper, we present a memory splitting transformation guided by a conservative memory analysis for Ethereum bytecode generated by the Solidity compiler. The analysis consists of two phases: recovering memory allocation and memory regions, followed by a pointer analysis. The goal of the analysis is to enable memory splitting which in turn speeds up verification. We have implemented both the analysis and the memory splitting transformation as part of a verification tool, CertoraProver, and show that the transformation speeds up SMT solving by up to 120\u00d7 and additionally mitigates 16 timeouts when used on 229 real-world smart contract verification tasks.<\/jats:p>","DOI":"10.1145\/3689796","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"2402-2433","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Practical Verification of Smart Contracts using Memory Splitting"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-7541-4195","authenticated-orcid":false,"given":"Shelly","family":"Grossman","sequence":"first","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-1015-1624","authenticated-orcid":false,"given":"John","family":"Toman","sequence":"additional","affiliation":[{"name":"Certora, Seattle, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9696-7157","authenticated-orcid":false,"given":"Alexander","family":"Bakst","sequence":"additional","affiliation":[{"name":"Certora, San Diego, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-9403-0637","authenticated-orcid":false,"given":"Sameer","family":"Arora","sequence":"additional","affiliation":[{"name":"Certora, Seattle, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0723-1309","authenticated-orcid":false,"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Certora, Tel Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8633-8413","authenticated-orcid":false,"given":"Chandrakana","family":"Nandi","sequence":"additional","affiliation":[{"name":"Certora, Seattle, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"2020. Solidity 0.8.0 Release Announcement. https:\/\/soliditylang.org\/blog\/2020\/12\/16\/solidity-v0.8.0-release-announcement\/."},{"key":"e_1_3_2_3_2","unstructured":"2020. Solidity Code Generation Bug Can Cause Memory Corruption. https:\/\/medium.com\/certora\/bug-disclosure-solidity-code-generation-bug-can-cause-memory-corruption-bf65468d2b34."},{"key":"e_1_3_2_4_2","unstructured":"2020. Solidity Empty Byte Array Copy Bug. https:\/\/soliditylang.org\/blog\/2020\/10\/19\/empty-byte-array-copy-bug\/."},{"key":"e_1_3_2_5_2","unstructured":"2021. Solidity ABI Decoder Bug For Multi-Dimensional Memory Arrays. https:\/\/soliditylang.org\/blog\/2021\/04\/21\/decoding-from-memory-bug\/."},{"key":"e_1_3_2_6_2","unstructured":"2022. Size Check Bug in Nested Calldata Array ABI-Reencoding. https:\/\/soliditylang.org\/blog\/2022\/05\/17\/calldata-reencode-size-check-bug\/."},{"key":"e_1_3_2_7_2","unstructured":"2024. Aave Liquidity Protocol. https:\/\/aave.com\/."},{"key":"e_1_3_2_8_2","unstructured":"2024. Balancer DEX App. https:\/\/balancer.fi\/."},{"key":"e_1_3_2_9_2","unstructured":"2024. A better smarter currency. https:\/\/makerdao.com\/en\/."},{"key":"e_1_3_2_10_2","doi-asserted-by":"crossref","unstructured":"2024. CertoraProver Artifact On ACM DL. https:\/\/doi.org\/10.1145\/3580439 10.1145\/3580439","DOI":"10.1145\/3580439"},{"key":"e_1_3_2_11_2","unstructured":"2024. Curve. https:\/\/balancer.fi\/."},{"key":"e_1_3_2_12_2","unstructured":"2024. Decentralized Perpetual Exchange. https:\/\/gmx.io\/."},{"key":"e_1_3_2_13_2","unstructured":"2024. Earn Borrow and Build on Morpho. https:\/\/morpho.org\/."},{"key":"e_1_3_2_14_2","unstructured":"2024. Liquid staking with stETH. https:\/\/lido.fi\/."},{"key":"e_1_3_2_15_2","unstructured":"2024. The modular lending platform. https:\/\/www.euler.finance\/."},{"key":"e_1_3_2_16_2","unstructured":"2024. Secure Money Markets For All Crypto Assets. https:\/\/www.silo.finance\/."},{"key":"e_1_3_2_17_2","unstructured":"2024. Smart Accounts to Own the Internet. https:\/\/safe.global\/."},{"key":"e_1_3_2_18_2","unstructured":"2024. Uniswap Protocol: Swap earn and build on the leading decentralized crypto trading protocol. https:\/\/uniswap.org\/."},{"key":"e_1_3_2_19_2","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/3-540-45789-5_18","volume-title":"Static Analysis","author":"Adams Stephen","year":"2002","unstructured":"Stephen Adams, Thomas Ball, Manuvir Das, Sorin Lerner, Sriram K. Rajamani, Mark Seigle, and Westley Weimer. 2002. Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis. In Static Analysis, Manuel V. Hermenegildo and Germ\u00e1n Puebla (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 230\u2013246."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_23"},{"issue":"4","key":"e_1_3_2_21_2","first-page":"29","article-title":"SuperOptimization of Smart Contracts","volume":"31","author":"Albert Elvira","year":"2022","unstructured":"Elvira Albert, Pablo Gordillo, Alejandro Hern\u00e1ndez-Cerezo, Albert Rubio, and Maria A. Schett. 2022. SuperOptimization of Smart Contracts. ACM Trans. Softw. Eng. Methodol. 31, 4, Article 70 (jul 2022), 29 pages. https:\/\/doi.org\/10.1145\/3506800 10.1145\/3506800","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"e_1_3_2_22_2","doi-asserted-by":"crossref","first-page":"513","DOI":"10.1007\/978-3-030-01090-4_30","volume-title":"Automated Technology for Verification and Analysis","author":"Albert Elvira","year":"2018","unstructured":"Elvira Albert, Pablo Gordillo, Benjamin Livshits, Albert Rubio, and Ilya Sergey. 2018. EthIR: A Framework for High-Level Analysis of Ethereum Bytecode. In Automated Technology for Verification and Analysis, Shuvendu K. Lahiri and Chao Wang (Eds.). Springer International Publishing, Cham, 513\u2013520."},{"key":"e_1_3_2_23_2","unstructured":"Elvira Albert Pablo Gordillo Albert Rubio and Ilya Sergey. 2018. Running on Fumes\u2013Preventing Out-of-Gas Vulnerabilities in Ethereum Smart Contracts using Static Resource Analysis. https:\/\/doi.org\/10.48550\/ARXIV.1811.10403 10.48550\/ARXIV.1811.10403"},{"key":"e_1_3_2_24_2","doi-asserted-by":"crossref","unstructured":"Leonardo Alt Martin Blicha Antti E. J. Hyv\u00e4rinen and Natasha Sharygina. 2022. SolCMC: Solidity Compiler\u2019s Model Checker. In Computer Aided Verification: 34th International Conference CAV 2022 Haifa Israel August 7\u201310 2022 Proceedings Part I (Haifa Israel). Springer-Verlag Berlin Heidelberg 325\u2013338. https:\/\/doi.org\/10.1007\/978-3-031-13185-1_16 10.1007\/978-3-031-13185-1_16","DOI":"10.1007\/978-3-031-13185-1_16"},{"key":"e_1_3_2_25_2","first-page":"376","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV","author":"Alt Leonardo","year":"2018","unstructured":"Leonardo Alt and Christian Reitwiessner. 2018. SMT-Based Verification of Solidity Smart Contracts. In Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV (Limassol, Cyprus). Springer-Verlag, Berlin, Heidelberg, 376\u2013388. https:\/\/doi.org\/10.1007\/978-3-030-03427-6_28 10.1007\/978-3-030-03427-6_28"},{"key":"e_1_3_2_26_2","unstructured":"Lars Ole Andersen. 1994. Program analysis and specialization for the C programming language. Ph. D. Dissertation. Citeseer."},{"key":"e_1_3_2_27_2","doi-asserted-by":"crossref","first-page":"1788","DOI":"10.1145\/3412841.3442051","volume-title":"Proceedings of the 36th Annual ACM Symposium on Applied ComputingSAC \u201921","author":"Antonino Pedro","year":"2021","unstructured":"Pedro Antonino and A. W. Roscoe. 2021. Solidifier: bounded model checking solidity using lazy contract deployment and precise memory modelling. In Proceedings of the 36th Annual ACM Symposium on Applied Computing (Virtual Event, Republic of Korea) (SAC \u201921). Association for Computing Machinery, New York, NY, USA, 1788\u20131797. https:\/\/doi.org\/10.1145\/3412841.3442051 10.1145\/3412841.3442051"},{"key":"e_1_3_2_28_2","doi-asserted-by":"crossref","unstructured":"Yulong Bao Xue-Yang Zhu Wenhui Zhang Wuwei Shen Pengfei Sun and Yingqi Zhao. 2022. On Verification of Smart Contracts via Model Checking. In Theoretical Aspects of Software Engineering Yamine A\u00eft-Ameur and Florin Cr\u0103ciun (Eds.). Springer International Publishing Cham 92\u2013112.","DOI":"10.1007\/978-3-031-10363-6_7"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/1108792.1108813"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032319"},{"key":"e_1_3_2_32_2","first-page":"30","article-title":"Rich specifications for Ethereum smart contract verification","volume":"5","author":"Br\u00e4m Christian","year":"2021","unstructured":"Christian Br\u00e4m, Marco Eilers, Peter M\u00fcller, Robin Sierra, and Alexander J. Summers. 2021. Rich specifications for Ethereum smart contract verification. Proc. ACM Program. Lang. 5, OOPSLA, Article 146 (oct 2021), 30 pages. https:\/\/doi.org\/10.1145\/3485523 10.1145\/3485523","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","first-page":"454","DOI":"10.1145\/3385412.3385990","volume-title":"Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and ImplementationPLDI 2020","author":"Brent Lexi","year":"2020","unstructured":"Lexi Brent, Neville Grech, Sifis Lagouvardos, Bernhard Scholz, and Yannis Smaragdakis. 2020. Ethainter: A Smart Contract Security Analyzer for Composite Vulnerabilities. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (London, UK) (PLDI 2020). Association for Computing Machinery, New York, NY, USA, 454\u2013469. https:\/\/doi.org\/10.1145\/3385412.3385990 10.1145\/3385412.3385990"},{"key":"e_1_3_2_34_2","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1007\/BFb0025882","volume-title":"Languages and Compilers for Parallel Computing","author":"Burke Michael","year":"1995","unstructured":"Michael Burke, Paul Carini, Jong-Deok Choi, and Michael Hind. 1995. Flow-insensitive interprocedural alias analysis in the presence of pointers. In Languages and Compilers for Parallel Computing, Keshav Pingali, Utpal Banerjee, David Gelernter, Alex Nicolau, and David Padua (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 234\u2013250."},{"key":"e_1_3_2_35_2","doi-asserted-by":"crossref","first-page":"571","DOI":"10.1007\/978-3-031-27481-7_32","volume-title":"Formal Methods: 25th International Symposium, FM 2023, L\u00fcbeck, Germany, March 6\u201310, 2023, Proceedings","author":"Cassez Franck","year":"2023","unstructured":"Franck Cassez, Joanne Fuller, Milad K. Ghale, David J. Pearce, and Horacio M. A. Quiles. 2023. Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. In Formal Methods: 25th International Symposium, FM 2023, L\u00fcbeck, Germany, March 6\u201310, 2023, Proceedings (L\u00fcbeck, Germany). Springer-Verlag, Berlin, Heidelberg, 571\u2013583. https:\/\/doi.org\/10.1007\/978-3-031-27481-7_32 10.1007\/978-3-031-27481-7_32"},{"key":"e_1_3_2_36_2","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/978-3-031-15008-1_5","volume-title":"Formal Methods for Industrial Critical Systems: 27th International Conference, FMICS 2022, Warsaw, Poland, September 14\u201315, 2022, Proceedings","author":"Cassez Franck","year":"2022","unstructured":"Franck Cassez, Joanne Fuller, and Horacio Mijail Ant\u00f3n Quiles. 2022. Deductive Verification of Smart Contracts with Dafny. In Formal Methods for Industrial Critical Systems: 27th International Conference, FMICS 2022, Warsaw, Poland, September 14\u201315, 2022, Proceedings (Warsaw, Poland). Springer-Verlag, Berlin, Heidelberg, 50\u201366. https:\/\/doi.org\/10.1007\/978-3-031-15008-1_5 10.1007\/978-3-031-15008-1_5"},{"key":"e_1_3_2_37_2","unstructured":"Certik. 2024. Certik. https:\/\/www.certik.com\/."},{"key":"e_1_3_2_38_2","unstructured":"Certora. 2024. Certora Prover Documentation. https:\/\/docs.certora.com\/en\/latest\/."},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2021.3054928"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158639"},{"key":"e_1_3_2_41_2","unstructured":"ConsenSys. 2024. Mythril: Security analysis tool for EVM bytecode. https:\/\/github.com\/Consensys\/mythril."},{"key":"e_1_3_2_42_2","unstructured":"Filippo Contro Marco Crosara Mariano Ceccato and Mila Dalla Preda. 2021. EtherSolve: Computing an Accurate Control-Flow Graph from Ethereum Bytecode. https:\/\/doi.org\/10.48550\/ARXIV.2103.09113 10.48550\/ARXIV.2103.09113"},{"key":"e_1_3_2_43_2","first-page":"613","volume-title":"Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software EngineeringASE 2017","author":"Coppa Emilio","year":"2017","unstructured":"Emilio Coppa, Daniele Cono D\u2019Elia, and Camil Demetrescu. 2017. Rethinking Pointer Reasoning in Symbolic Execution. In Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering (Urbana-Champaign, IL, USA) (ASE 2017). IEEE Press, 613\u2013618."},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_3_2_45_2","doi-asserted-by":"crossref","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice of Software 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest Hungary) (TACAS\u201908\/ETAPS\u201908). Springer-Verlag Berlin Heidelberg 337\u2013340. http:\/\/dl.acm.org\/citation.cfm?id=1792734.1792766","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_46_2","doi-asserted-by":"crossref","unstructured":"Monika di Angelo and Gernot Salzer. 2019. A Survey of Tools for Analyzing Ethereum Smart Contracts. In 2019 IEEE International Conference on Decentralized Applications and Infrastructures (DAPPCON). 69\u201378. https:\/\/doi.org\/10.1109\/DAPPCON.2019.00018 10.1109\/DAPPCON.2019.00018","DOI":"10.1109\/DAPPCON.2019.00018"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"e_1_3_2_48_2","unstructured":"EBPF. 2024. Dynamically program the kernel for efficient networking observability tracing and security. https:\/\/ebpf.io\/."},{"key":"e_1_3_2_49_2","first-page":"363","volume-title":"LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (EPiC Series in Computing, Vol. 57)","author":"Farinier Benjamin","year":"2018","unstructured":"Benjamin Farinier, Robin David, S\\\u2019ebastien Bardin, and Matthieu Lemerre. 2018. Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing. In LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (EPiC Series in Computing, Vol. 57), Gilles Barthe, Geoff Sutcliffe, and Margus Veanes (Eds.). EasyChair, 363\u2013380. https:\/\/doi.org\/10.29007\/dc9b 10.29007\/dc9b"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416646"},{"key":"e_1_3_2_51_2","first-page":"18","volume-title":"Proceedings of the 29th USENIX Conference on Security Symposium (SEC\u201920)","author":"Frank Joel","year":"2020","unstructured":"Joel Frank, Cornelius Aschermann, and Thorsten Holz. 2020. ETHBMC: A Bounded Model Checker for Smart Contracts. In Proceedings of the 29th USENIX Conference on Security Symposium (SEC\u201920). USENIX Association, USA, Article 155, 18 pages."},{"key":"e_1_3_2_52_2","unstructured":"Ghidra. 2024. A software reverse engineering (SRE) suite of tools developed by NSA\u2019s Research Directorate in support of the Cybersecurity mission. https:\/\/ghidra-sre.org."},{"key":"e_1_3_2_53_2","doi-asserted-by":"crossref","unstructured":"Neville Grech Lexi Brent Bernhard Scholz and Yannis Smaragdakis. 2019. Gigahorse: Thorough Declarative Decompilation of Smart Contracts. In 2019 IEEE\/ACM 41st International Conference on Software Engineering (ICSE). 1176\u20131186. https:\/\/doi.org\/10.1109\/ICSE.2019.00120 10.1109\/ICSE.2019.00120","DOI":"10.1109\/ICSE.2019.00120"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3416262"},{"key":"e_1_3_2_55_2","doi-asserted-by":"crossref","unstructured":"Neville Grech Sifis Lagouvardos Ilias Tsatiris and Yannis Smaragdakis. 2022. Elipmoc: Advanced Decompilation of Ethereum Smart Contracts. Proc. ACM Program. Lang. 6 OOPSLA1 Article 77 (apr 2022) 27 pages. https:\/\/doi.org\/10.1145\/3527321 10.1145\/3527321","DOI":"10.1145\/3527321"},{"key":"e_1_3_2_56_2","first-page":"243","volume-title":"Principles of Security and Trust","author":"Grishchenko Ilya","year":"2018","unstructured":"Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018. A Semantic Framework for the Security Analysis of Ethereum Smart Contracts. In Principles of Security and Trust, Lujo Bauer and Ralf K\u00fcsters (Eds.). Springer International Publishing, Cham, 243\u2013269."},{"key":"e_1_3_2_57_2","unstructured":"I. Grishchenko Matteo Maffei and Clara Schneidewind. 2022. EtherTrust: Sound Static Analysis of Ethereum bytecode. https:\/\/www.netidee.at\/sites\/default\/files\/2018-07\/staticanalysis.pdf."},{"key":"e_1_3_2_58_2","first-page":"28","article-title":"Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts","volume":"2","author":"Grossman Shelly","year":"2017","unstructured":"Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar. 2017. Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts. Proc. ACM Program. Lang. 2, POPL, Article 48 (dec 2017), 28 pages. https:\/\/doi.org\/10.1145\/3158136 10.1145\/3158136","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_8"},{"key":"e_1_3_2_60_2","first-page":"161","volume-title":"solc-verify: A Modular Verifier for Solidity Smart Contracts.","author":"Hajdu \u00c1kos","year":"2020","unstructured":"\u00c1kos Hajdu and Dejan Jovanovi\u0107. 2020. solc-verify: A Modular Verifier for Solidity Smart Contracts. Springer International Publishing, 161\u2013179. https:\/\/doi.org\/10.1007\/978-3-030-41600-3_11 10.1007\/978-3-030-41600-3_11"},{"key":"e_1_3_2_61_2","unstructured":"Team Halmos. 2024. Halmos: A symbolic testing tool for EVM smart contracts. https:\/\/github.com\/a16z\/halmos."},{"key":"e_1_3_2_62_2","unstructured":"Team HEVM. 2024. HEVM: Symbolic EVM Evaluator. https:\/\/github.com\/ethereum\/hevm."},{"key":"e_1_3_2_63_2","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1145\/379605.379665","volume-title":"Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and EngineeringPASTE \u201901)","author":"Hind Michael","year":"2001","unstructured":"Michael Hind. 2001. Pointer Analysis: Haven\u2019t We Solved This Problem Yet?. In Proceedings of the 2001 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (Snowbird, Utah, USA) (PASTE \u201901). Association for Computing Machinery, New York, NY, USA, 54\u201361. https:\/\/doi.org\/10.1145\/379605.379665 10.1145\/379605.379665"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/347636.348916"},{"issue":"14","key":"e_1_3_2_65_2","first-page":"37","article-title":"Security Threat Mitigation for Smart Contracts: A Comprehensive Survey","volume":"55","author":"Ivanov Nikolay","year":"2023","unstructured":"Nikolay Ivanov, Chenning Li, Qiben Yan, Zhiyuan Sun, Zhichao Cao, and Xiapu Luo. 2023. Security Threat Mitigation for Smart Contracts: A Comprehensive Survey. ACM Comput. Surv. 55, 14s, Article 326 (jul 2023), 37 pages. https:\/\/doi.org\/10.1145\/3593293 10.1145\/3593293","journal-title":"ACM Comput. Surv."},{"key":"e_1_3_2_66_2","first-page":"259","volume-title":"ContractFuzzer: Fuzzing Smart Contracts for Vulnerability Detection.","author":"Jiang Bo","year":"2018","unstructured":"Bo Jiang, Ye Liu, and W. K.Chan. 2018. ContractFuzzer: Fuzzing Smart Contracts for Vulnerability Detection. Association for Computing Machinery, New York, NY, USA, 259\u2013269. https:\/\/doi.org\/10.1145\/3238147.3238177 10.1145\/3238147.3238177"},{"key":"e_1_3_2_67_2","doi-asserted-by":"crossref","unstructured":"Sukrit Kalra Seep Goel Mohan Dhawan and Subodh Sharma. 2018. Zeus: analyzing safety of smart contracts.. In Ndss. 1\u201312.","DOI":"10.14722\/ndss.2018.23082"},{"key":"e_1_3_2_68_2","unstructured":"KEVM. 2024. K Semantics of the Ethereum Virtual Machine (EVM). https:\/\/github.com\/runtimeverification\/evm-semantics."},{"key":"e_1_3_2_69_2","first-page":"26","article-title":"Precise Static Modeling of Ethereum \u201cMemory\u201d","volume":"4","author":"Lagouvardos Sifis","year":"2020","unstructured":"Sifis Lagouvardos, Neville Grech, Ilias Tsatiris, and Yannis Smaragdakis. 2020. Precise Static Modeling of Ethereum \u201cMemory\u201d. Proc. ACM Program. Lang. 4, OOPSLA, Article 190 (nov 2020), 26 pages. https:\/\/doi.org\/10.1145\/3428258 10.1145\/3428258","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_2_70_2","doi-asserted-by":"crossref","unstructured":"Rustan Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In 16th International Conference LPAR-16 Dakar Senegal (16th international conference lpar-16 dakar senegal ed.). Springer Berlin Heidelberg 348\u2013370. https:\/\/www.microsoft.com\/en-us\/research\/publication\/dafny-automatic-program-verifier-functional-correctness-2\/","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_72_2","first-page":"178","volume-title":"In Leveraging Applications of Formal Methods, Verification and Validation: Applications: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20\u201330, 2020, Proceedings, Part III","author":"Marescotti Matteo","year":"2020","unstructured":"Matteo Marescotti, Rodrigo Otoni, Leonardo Alt, Patrick Eugster, Antti E. J. Hyv\u00e4rinen, and Natasha Sharygina. 2020. Accurate Smart Contract Verification Through Direct Modelling. In Leveraging Applications of Formal Methods, Verification and Validation: Applications: 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Rhodes, Greece, October 20\u201330, 2020, Proceedings, Part III (Rhodes, Greece). Springer-Verlag, Berlin, Heidelberg, 178\u2013194. https:\/\/doi.org\/10.1007\/978-3-030-61467-6_12 10.1007\/978-3-030-61467-6_12"},{"key":"e_1_3_2_73_2","unstructured":"Anastasia Mavridou and Aron Laszka. 2017. Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach. CoRR abs\/1711.09327 (2017). arXiv:1711.09327 http:\/\/arxiv.org\/abs\/1711.09327"},{"key":"e_1_3_2_74_2","doi-asserted-by":"crossref","unstructured":"Anastasia Mavridou Aron Laszka Stachtiari Emmanouela and Abhishek Dubey. 2019. VeriSolid: Correct-by-Design Smart Contracts for Ethereum. In Proceedings of the 23nd International Conference on Financial Cryptography and Data Security (FC).","DOI":"10.1007\/978-3-030-32101-7_27"},{"key":"e_1_3_2_75_2","unstructured":"John McCarthy. 1962. Towards a Mathematical Science of Computation. In Information Processing Proceedings of the 2nd IFIP Congress 1962 Munich Germany August 27 - September 1 1962. North-Holland 21\u201328."},{"key":"e_1_3_2_76_2","unstructured":"Move. 2024. Move. https:\/\/move-book.com\/."},{"key":"e_1_3_2_77_2","doi-asserted-by":"crossref","unstructured":"Zeinab Neha\u00ef Pierre-Yves Piriou and Fr\u00e9d\u00e9ric Daumas. 2018. Model-Checking of Smart Contracts. In 2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData). 980\u2013987. https:\/\/doi.org\/10.1109\/Cybermatics_2018.2018.00185 10.1109\/Cybermatics_2018.2018.00185","DOI":"10.1109\/Cybermatics_2018.2018.00185"},{"key":"e_1_3_2_78_2","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274743"},{"key":"e_1_3_2_79_2","doi-asserted-by":"crossref","first-page":"1661","DOI":"10.1109\/SP40000.2020.00024","volume-title":"2020 IEEE symposium on security and privacy (SP)","author":"Permenev Anton","year":"2020","unstructured":"Anton Permenev, Dimitar Dimitrov, Petar Tsankov, Dana Drachsler-Cohen, and Martin Vechev. 2020. Verx: Safety verification of smart contracts. In 2020 IEEE symposium on security and privacy (SP). IEEE, 1661\u20131677."},{"key":"e_1_3_2_80_2","unstructured":"IDA Pro. 2024. A powerful disassembler and a versatile debugger. https:\/\/hex-rays.com\/ida-pro."},{"key":"e_1_3_2_81_2","unstructured":"Rust. 2024. Rust. https:\/\/www.rust-lang.org\/."},{"key":"e_1_3_2_82_2","unstructured":"RV. 2022. Runtime Verification. https:\/\/runtimeverification.com\/."},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.1145\/271510.271517"},{"key":"e_1_3_2_84_2","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292552"},{"key":"e_1_3_2_85_2","doi-asserted-by":"crossref","unstructured":"Clara Schneidewind Ilya Grishchenko Markus Scherer and Matteo Maffei. 2020. eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. arXiv:2005.06227 [cs.PL]","DOI":"10.1145\/3372297.3417250"},{"key":"e_1_3_2_86_2","first-page":"30","article-title":"Safer Smart Contract Programming with Scilla","volume":"3","author":"Sergey Ilya","year":"2019","unstructured":"Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, and Ken Chan Guan Hao. 2019. Safer Smart Contract Programming with Scilla. Proc. ACM Program. Lang. 3, OOPSLA, Article 185 (oct 2019), 30 pages. https:\/\/doi.org\/10.1145\/3360611 10.1145\/3360611","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_2_87_2","first-page":"30","article-title":"Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts","volume":"5","author":"Smaragdakis Yannis","year":"2021","unstructured":"Yannis Smaragdakis, Neville Grech, Sifis Lagouvardos, Konstantinos Triantafyllou, and Ilias Tsatiris. 2021. Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts. Proc. ACM Program. Lang. 5, OOPSLA, Article 163 (oct 2021), 30 pages. https:\/\/doi.org\/10.1145\/3485540 10.1145\/3485540","journal-title":"Proc. ACM Program. Lang."},{"key":"e_1_3_2_88_2","first-page":"1678","article-title":"VERISMART: A Highly Precise Safety Verifier for Ethereum Smart Contracts","author":"So Sunbeom","year":"2020","unstructured":"Sunbeom So, Myungho Lee, Jisu Park, Heejo Lee, and Hakjoo Oh. 2020. VERISMART: A Highly Precise Safety Verifier for Ethereum Smart Contracts. In 2020 IEEE Symposium on Security and Privacy (SP). 1678\u20131694. https:\/\/doi.org\/10.1109\/SP40000.2020.00032 10.1109\/SP40000.2020.00032","journal-title":"2020 IEEE Symposium on Security and Privacy (SP)"},{"key":"e_1_3_2_89_2","unstructured":"Solidity. 2024. Solidity. https:\/\/soliditylang.org\/."},{"key":"e_1_3_2_90_2","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1145\/3510454.3516855","volume-title":"Proceedings of the ACM\/IEEE 44th International Conference on Software Engineering: Companion ProceedingsICSE \u201922)","author":"Song Kunjian","year":"2022","unstructured":"Kunjian Song, Nedas Matulevicius, Eddie B. de Lima Filho, and Lucas C. Cordeiro. 2022. ESBMC-solidity: an SMT-based model checker for solidity smart contracts. In Proceedings of the ACM\/IEEE 44th International Conference on Software Engineering: Companion Proceedings (Pittsburgh, Pennsylvania) (ICSE \u201922). Association for Computing Machinery, New York, NY, USA, 65\u201369. https:\/\/doi.org\/10.1145\/3510454.3516855 10.1145\/3510454.3516855"},{"key":"e_1_3_2_91_2","unstructured":"Souffle. 2024. Souffle. https:\/\/souffle-lang.github.io\/index.html."},{"key":"e_1_3_2_92_2","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237727"},{"key":"e_1_3_2_93_2","unstructured":"Ryan Stortz. 2022. Rattle \u2013 an Ethereum EVM binary analysis framework. https:\/\/blog.trailofbits.com\/2018\/09\/06\/rattle-an-ethereum-evm-binary-analysis-framework\/."},{"key":"e_1_3_2_94_2","doi-asserted-by":"crossref","unstructured":"Bryan Tan Benjamin Mariano Shuvendu K. Lahiri Isil Dillig and Yu Feng. 2022. SolType: Refinement Types for Arithmetic Overflow in Solidity. Proc. ACM Program. Lang. 6 POPL Article 4 (jan 2022) 29 pages. https:\/\/doi.org\/10.1145\/3498665 10.1145\/3498665","DOI":"10.1145\/3498665"},{"key":"e_1_3_2_95_2","first-page":"67","volume-title":"Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications SecurityCCS \u201918)","author":"Tsankov Petar","year":"2018","unstructured":"Petar Tsankov, Andrei Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian B\u00fcnzli, and Martin Vechev. 2018. Securify: Practical Security Analysis of Smart Contracts. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (Toronto, Canada) (CCS \u201918). Association for Computing Machinery, New York, NY, USA, 67\u201382. https:\/\/doi.org\/10.1145\/3243734.3243780 10.1145\/3243734.3243780"},{"key":"e_1_3_2_96_2","first-page":"13","volume-title":"Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative ResearchCASCON \u201999)","author":"Vall\u00e9e-Rai Raja","year":"1999","unstructured":"Raja Vall\u00e9e-Rai, Phong Co, Etienne Gagnon, Laurie Hendren, Patrick Lam, and Vijay Sundaresan. 1999. Soot - a Java Bytecode Optimization Framework. In Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research (Mississauga, Ontario, Canada) (CASCON \u201999). IBM Press, 13."},{"key":"e_1_3_2_97_2","unstructured":"Runtime Verification. 2024. The K Framework. https:\/\/kframework.org\/."},{"key":"e_1_3_2_98_2","unstructured":"Vyper. 2024. Vyper. https:\/\/vyper.readthedocs.io\/en\/stable\/."},{"key":"e_1_3_2_99_2","doi-asserted-by":"crossref","first-page":"539","DOI":"10.1007\/978-3-319-52234-0_29","volume-title":"Verification, Model Checking, and Abstract Interpretation: 18th International Conference, VMCAI 2017, Paris, France, January 15\u201317, 2017, Proceedings 18.","author":"Wang Wei","year":"2017","unstructured":"Wei Wang, Clark Barrett, and Thomas Wies. 2017. Partitioned memory models for program analysis. In Verification, Model Checking, and Abstract Interpretation: 18th International Conference, VMCAI 2017, Paris, France, January 15\u201317, 2017, Proceedings 18. Springer, 539\u2013558."},{"key":"e_1_3_2_100_2","doi-asserted-by":"crossref","unstructured":"Yuepeng Wang Shuvendu K. Lahiri Shuo Chen Rong Pan Isil Dillig Cody Born and Immad Naseer. 2019. Formal Specification and Verification of Smart Contracts for Azure Blockchain. arXiv:1812.08829 [cs.PL]","DOI":"10.1007\/978-3-030-41600-3_7"},{"key":"e_1_3_2_101_2","unstructured":"wasm. 2024. wasm. https:\/\/webassembly.org\/."},{"key":"e_1_3_2_102_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88806-0_21"},{"key":"e_1_3_2_103_2","first-page":"715","volume-title":"Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings (Lecture Notes in Computer Science, Vol. 5643)","author":"Wintersteiger Christoph M.","year":"2009","unstructured":"Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo Mendon\u00e7a de Moura. 2009. A Concurrent Portfolio Approach to SMT Solving. In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings (Lecture Notes in Computer Science, Vol. 5643), Ahmed Bouajjani and Oded Maler (Eds.). Springer, 715\u2013720. https:\/\/doi.org\/10.1007\/978-3-642-02658-4_60 10.1007\/978-3-642-02658-4_60"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689796","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689796","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:13:47Z","timestamp":1770196427000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689796"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":102,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689796"],"URL":"https:\/\/doi.org\/10.1145\/3689796","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}