{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:32:38Z","timestamp":1755999158921,"version":"3.41.0"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2025,2,7]],"date-time":"2025-02-07T00:00:00Z","timestamp":1738886400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Information Technology Lab of National Institute of Standards and Technology","award":["70NANB21H092"],"award-info":[{"award-number":["70NANB21H092"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Distrib. Ledger Technol."],"published-print":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>Symbolic execution of smart contracts suffers from sequence explosion. Some existing tools limit the sequence length, thus being unable to adequately evaluate some functions. In this article, we propose a symbolic execution approach without limiting the sequence length. In our approach, the symbolic execution process is a two-phase model that maximizes code coverage while reducing the number of sequences to be executed. The first phase executes all sequences up to a length limit to identify the not-fully covered functions, while the second attempts to cover these functions according to state evaluation and a function graph structure. We have developed a tool called SmartExecutor and conducted an experimental evaluation on the SGUARD dataset. The experimental results indicate that compared with state-of-the-art tools, SmartExecutor achieves higher code coverage with less time. It also detects more vulnerabilities than Mythril, a state-of-the-art symbolic execution tool.<\/jats:p>","DOI":"10.1145\/3678188","type":"journal-article","created":{"date-parts":[[2024,7,15]],"date-time":"2024-07-15T16:07:21Z","timestamp":1721059641000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["SmartExecutor: Coverage-Driven Symbolic Execution Guided via State Prioritization and Function Selection"],"prefix":"10.1145","volume":"4","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-1369-7415","authenticated-orcid":false,"given":"Qiping","family":"Wei","sequence":"first","affiliation":[{"name":"Department of Computer Science and Engineering, The University of Texas at Arlington, Arlington, TX, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-8876-1219","authenticated-orcid":false,"given":"Fadul","family":"Sikder","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, The University of Texas at Arlington, Arlington, TX, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3613-1577","authenticated-orcid":false,"given":"Huadong","family":"Feng","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, The University of Texas at Arlington, Arlington, TX, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1069-5980","authenticated-orcid":false,"given":"Yu","family":"Lei","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, The University of Texas at Arlington, Arlington, TX, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7666-3391","authenticated-orcid":false,"given":"Raghu","family":"Kacker","sequence":"additional","affiliation":[{"name":"National Institute of Standards and Technology, Gaithersburg, MD, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0050-1596","authenticated-orcid":false,"given":"Richard","family":"Kuhn","sequence":"additional","affiliation":[{"name":"National Institute of Standards and Technology, Gaithersburg, MD, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,2,7]]},"reference":[{"key":"e_1_3_2_2_2","first-page":"227","volume-title":"Proceedings of the 2021 36th IEEE\/ACM International Conference on Automated Software Engineering (ASE)","author":"Choi Jaeseung","year":"2021","unstructured":"Jaeseung Choi, Doyeon Kim, Soomin Kim, Gustavo Grieco, Alex Groce, and Sang Kil Cha. 2021. SMARTIAN: Enhancing smart contract fuzzing with static and dynamic data-flow analyses. In Proceedings of the 2021 36th IEEE\/ACM International Conference on Automated Software Engineering (ASE). 227\u2013239. https:\/\/doi.org\/10.1109\/ASE51524.2021.9678888"},{"unstructured":"ConsenSys. 2015. ConsenSys Is a Market-Leading Blockchain Technology Company. Retrieved November 20 2023 from https:\/\/consensys.net\/about\/","key":"e_1_3_2_3_2"},{"unstructured":"contractAnalysis. 2023. Case Studies on Mpro. Retrieved from https:\/\/github.com\/contractAnalysis\/smartExecutor_exp_data\/tree\/smartExecutor_paper\/mpro_case_study","key":"e_1_3_2_4_2"},{"unstructured":"contractAnalysis. 2023. SmartExecutor. Retrieved from https:\/\/github.com\/contractAnalysis\/smartExecutor","key":"e_1_3_2_5_2"},{"unstructured":"contractAnalysis. 2023c. SmartExecutor Experiment Data Preparation. Retrieved from https:\/\/github.com\/contractAnalysis\/smartExecutor_exp_data","key":"e_1_3_2_6_2"},{"unstructured":"Joseph Cook. 2023. Ethereum Accounts. Retrieved November 20 2023 from https:\/\/ethereum.org\/en\/developers\/docs\/accounts\/","key":"e_1_3_2_7_2"},{"unstructured":"ConsenSys Diligence. 2019. Analysis Modules (Detection Capabilities). Retrieved from https:\/\/mythril-classic.readthedocs.io\/en\/master\/analysis-modules.html","key":"e_1_3_2_8_2"},{"unstructured":"Ethereum. 2016. Solidity. Retrieved November 20 2023 from https:\/\/docs.soliditylang.org\/en\/v0.8.7\/","key":"e_1_3_2_9_2"},{"unstructured":"Etherscan. 2015. The Ethereum Blockchain Explorer. Retrieved November 20 2023 from https:\/\/etherscan.io\/","key":"e_1_3_2_10_2"},{"key":"e_1_3_2_11_2","volume-title":"Proceedings of the 34nd IEEE\/ACM International Conference on Automated Software Engineering (ASE \u201919)","author":"Feist Josselin","year":"2019","unstructured":"Josselin Feist, Gustavo Greico, and Alex Groce. 2019. Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. In Proceedings of the 34nd IEEE\/ACM International Conference on Automated Software Engineering (ASE \u201919)."},{"unstructured":"Shane Fontaine. 2019. Understanding Bytecode on Ethereum. Retrieved November 20 2023 from https:\/\/medium.com\/authereum\/bytecode-and-init-code-and-runtime-code-oh-my-7bcd89065904","key":"e_1_3_2_12_2"},{"unstructured":"fravoll. 2018. Tight Variable Packing. Retrieved November 19 2023 from https:\/\/fravoll.github.io\/solidity-patterns\/tight_variable_packing.html","key":"e_1_3_2_13_2"},{"key":"e_1_3_2_14_2","volume-title":"Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis","author":"Ghaleb Asem","year":"2020","unstructured":"Asem Ghaleb and Karthik Pattabiraman. 2020. Slither: A static analysis framework for smart contracts. In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis."},{"unstructured":"Masoud Ghorbanzadeh. 2023. Transactions. Retrieved November 20 2023 from https:\/\/ethereum.org\/en\/developers\/docs\/transactions\/","key":"e_1_3_2_15_2"},{"key":"e_1_3_2_16_2","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."},{"doi-asserted-by":"publisher","key":"e_1_3_2_17_2","DOI":"10.1145\/3319535.3363230"},{"unstructured":"Holo. 2018. Token HoloToken. Retrieved November 20 2023 from https:\/\/etherscan.io\/token\/0x6c6ee5e31d828de241282b9606c8e98ea48526e2","key":"e_1_3_2_18_2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_19_2","DOI":"10.1109\/TC.2021.3092639"},{"unstructured":"Sylabs Inc. 2017. Apptainer User Guide. Retrieved November 20 2023 from https:\/\/apptainer.org\/docs\/user\/latest\/","key":"e_1_3_2_20_2"},{"unstructured":"Wayne Jones. 2022. The DAO Attack: Understanding What Happened. Retrieved from https:\/\/crypto.news\/learn\/the-dao-attack-understanding-what-happened\/","key":"e_1_3_2_21_2"},{"key":"e_1_3_2_22_2","volume-title":"Proceedings of the 27th USENIX Conference on Security Symposium","author":"Krupp Johannes","year":"2018","unstructured":"Johannes Krupp and Christian Rossow. 2018. TEETHER: Gnawing at ethereum to automatically exploit smart contracts. In Proceedings of the 27th USENIX Conference on Security Symposium."},{"issue":"10","key":"e_1_3_2_23_2","first-page":"2065","article-title":"NeuCheck: A more practical ethereum smart contract security analysis tool","volume":"51","author":"Lu Ning","year":"2019","unstructured":"Ning Lu, Bin Wang, Yongxin Zhang, Wenbo Shi, and Christian Esposito. 2019. NeuCheck: A more practical ethereum smart contract security analysis tool. Software: Practice and Experience 51, 10 (2019), 2065\u20132084.","journal-title":"Software: Practice and Experience"},{"unstructured":"Bernhard Mueller. 2018. Smashing Ethereum Smart Contracts for Fun and Real Profit. Retrieved November 20 2023 from https:\/\/tinyurl.com\/y827tk72","key":"e_1_3_2_24_2"},{"unstructured":"Bernhard Mueller. 2018. Smashing Smart Contracts. Retrieved from https:\/\/github.com\/muellerberndt\/smashing-smart-contracts\/blob\/master\/smashing-smart-contracts-1of1.pdf","key":"e_1_3_2_25_2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_26_2","DOI":"10.1109\/SP40001.2021.00057"},{"unstructured":"Chigozie Oduah. 2023. What Are Solidity Modifiers? Explained with Examples. Retrieved November 20 2023 from https:\/\/www.freecodecamp.org\/news\/what-are-solidity-modifiers\/","key":"e_1_3_2_27_2"},{"unstructured":"Trail of Bits. 2019. A Symbolic Execution Tool for Analysis of Smart Contracts and Binaries. Retrieved from https:\/\/github.com\/trailofbits\/manticore","key":"e_1_3_2_28_2"},{"unstructured":"The University of Texas at Austin. 2024. Texas Advanced Computing Center (TACC). Retrieved from http:\/\/www.tacc.utexas.edu","key":"e_1_3_2_29_2"},{"unstructured":"Bernard Peh. 2017. Solidity Bytecode and Opcode Basics. Retrieved November 20 2023 from https:\/\/medium.com\/@blockchain101\/solidity-bytecode-and-opcode-basics-672e9b1a88c2","key":"e_1_3_2_30_2"},{"unstructured":"rakita. 2023. Ethereum Virtual Machine (EVM). Retrieved November 20 2023 from https:\/\/ethereum.org\/en\/developers\/docs\/evm\/","key":"e_1_3_2_31_2"},{"key":"e_1_3_2_32_2","volume-title":"Proceedings of the 30th USENIX Security Symposium","author":"So Sunbeom","year":"2021","unstructured":"Sunbeom So, Seongjoon Hong, and Hakjoo Oh. 2021. SmarTest: Effectively hunting vulnerable transaction sequences in smart contracts through language model-guided symbolic execution. In Proceedings of the 30th USENIX Security Symposium."},{"unstructured":"ConsenSys Software. 2018. A Security Analysis Tool for EVM Bytecode. Retrieved from https:\/\/github.com\/ConsenSys\/mythril","key":"e_1_3_2_33_2"},{"key":"e_1_3_2_34_2","volume-title":"Proceedings of the 5th Conference on Blockchain Research & Applications for Innovative Networks and Services (BRAINS)","author":"Wei Qiping","year":"2023","unstructured":"Qiping Wei, Fadul Sikder, Huadong Feng, Yu Lei, Raghu Kacker, and Richard Kuhn. 2023. SmartExecutor: Coverage-driven symbolic execution guided by a function dependency graph. In Proceedings of the 5th Conference on Blockchain Research & Applications for Innovative Networks and Services (BRAINS)."},{"doi-asserted-by":"publisher","key":"e_1_3_2_35_2","DOI":"10.1109\/IWBOSE.2018.8327565"},{"unstructured":"GAVIN WOOD. 2022. Ethereum Yellow Paper. Retrieved from https:\/\/ethereum.github.io\/yellowpaper\/paper.pdf","key":"e_1_3_2_36_2"},{"unstructured":"Xiao Liang Yu. 2017. An Analysis Tool for Smart Contracts. Retrieved from https:\/\/github.com\/enzymefinance\/oyente","key":"e_1_3_2_37_2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_38_2","DOI":"10.1145\/3431726"},{"doi-asserted-by":"publisher","key":"e_1_3_2_39_2","DOI":"10.1109\/ISSRE.2019.00052"},{"doi-asserted-by":"publisher","key":"e_1_3_2_40_2","DOI":"10.1016\/j.future.2019.12.019"}],"container-title":["Distributed Ledger Technologies: Research and Practice"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3678188","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3678188","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:08Z","timestamp":1750287248000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3678188"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,7]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,3,31]]}},"alternative-id":["10.1145\/3678188"],"URL":"https:\/\/doi.org\/10.1145\/3678188","relation":{},"ISSN":["2769-6480"],"issn-type":[{"type":"electronic","value":"2769-6480"}],"subject":[],"published":{"date-parts":[[2025,2,7]]},"assertion":[{"value":"2023-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-19","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-07","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}