{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T08:04:19Z","timestamp":1764403459363,"version":"build-2065373602"},"reference-count":216,"publisher":"MDPI AG","issue":"6","license":[{"start":{"date-parts":[[2025,6,9]],"date-time":"2025-06-09T00:00:00Z","timestamp":1749427200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Computers"],"abstract":"<jats:p>Smart contracts are self-executing programs that facilitate trustless transactions between multiple parties, most commonly deployed on the Ethereum blockchain. They have become integral to decentralized applications in areas such as voting, digital agreements, and financial systems. However, the immutable and transparent nature of smart contracts makes security vulnerabilities especially critical, as deployed contracts cannot be modified. Security flaws have led to substantial financial losses, underscoring the need for robust verification before deployment. This survey presents a comprehensive review of the state of the art in smart contract security verification, with a focus on Ethereum. We analyze a wide range of verification methods, including static and dynamic analysis, formal verification, and machine learning, and evaluate 62 open-source tools across their detection accuracy, efficiency, and usability. In addition, we highlight emerging trends, challenges, and the need for cross-methodological integration and benchmarking. Our findings aim to guide researchers, developers, and security auditors in selecting and advancing effective verification approaches for building secure and reliable smart contracts.<\/jats:p>","DOI":"10.3390\/computers14060226","type":"journal-article","created":{"date-parts":[[2025,6,9]],"date-time":"2025-06-09T08:22:34Z","timestamp":1749457354000},"page":"226","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Ethereum Smart Contracts Under Scrutiny: A Survey of Security Verification Tools, Techniques, and Challenges"],"prefix":"10.3390","volume":"14","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-5636-7062","authenticated-orcid":false,"given":"Mounira","family":"Kezadri Hamiaz","sequence":"first","affiliation":[{"name":"Computer Science and Information Department, Applied College, Taibah University, Madinah 42353, Saudi Arabia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8236-8746","authenticated-orcid":false,"given":"Maha","family":"Driss","sequence":"additional","affiliation":[{"name":"Robotics and Internet-of-Things Laboratory, Computer Science Department, College of Computer and Information Sciences, Prince Sultan University, Riyadh 11586, Saudi Arabia"}]}],"member":"1968","published-online":{"date-parts":[[2025,6,9]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","first-page":"61048","DOI":"10.1109\/ACCESS.2021.3072849","article-title":"A Survey on Blockchain Technology: Evolution, Architecture and Security","volume":"9","author":"Bhutta","year":"2021","journal-title":"IEEE Access"},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Hasan, D., and Driss, M. (December, January 30). SUBL\u03bcME: Secure blockchain as a service and microservices-based framework for IoT environments. Proceedings of the 2021 IEEE\/ACS 18th International Conference on Computer Systems and Applications (AICCSA), Tangier, Morocco.","DOI":"10.1109\/AICCSA53542.2021.9686757"},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Sadad, A., Khan, M.A., Ghaleb, B., Khan, F.A., Driss, M., Boulila, W., and Ahmad, J. (2023, January 19\u201323). Distributed twins in edge computing: Blockchain and IOTA. Proceedings of the 2023 International Wireless Communications and Mobile Computing (IWCMC), Marrakesh, Morocco.","DOI":"10.1109\/IWCMC58020.2023.10182509"},{"key":"ref_4","first-page":"154053","article-title":"UAVs and Blockchain Synergy: Enabling Secure Reputation-based Federated Learning in Smart Cities","volume":"12","author":"Abbas","year":"2024","journal-title":"IEEE Access"},{"key":"ref_5","doi-asserted-by":"crossref","unstructured":"Wadhwa, S., Gupta, D., Rani, S., Driss, M., and Boulila, W. (2025). Empowering drones in vehicular network through fog computing and blockchain technology. PLoS ONE, 20.","DOI":"10.1371\/journal.pone.0314420"},{"key":"ref_6","doi-asserted-by":"crossref","first-page":"87643","DOI":"10.1109\/ACCESS.2021.3068178","article-title":"Survey on blockchain-based smart contracts: Technical aspects and future research","volume":"9","author":"Hewa","year":"2021","journal-title":"IEEE Access"},{"key":"ref_7","unstructured":"Flipside Crypto (2024, May 01). Flipside|The Platform for Intelligent Blockchain Growth. Available online: https:\/\/flipsidecrypto.xyz\/."},{"key":"ref_8","doi-asserted-by":"crossref","first-page":"19","DOI":"10.4018\/JCIT.2019010102","article-title":"Understanding a revolutionary and flawed grand experiment in blockchain: The DAO attack","volume":"21","author":"Mehar","year":"2019","journal-title":"J. Cases Inf. Technol."},{"key":"ref_9","unstructured":"Palladino, S. (2025, May 30). The Parity Wallet Hack Explained. Available online: https:\/\/blog.openzeppelin.com\/on-the-parity-wallet-multisig-hack-405a8c12e8f7."},{"key":"ref_10","doi-asserted-by":"crossref","first-page":"100021","DOI":"10.1016\/j.bcra.2021.100021","article-title":"A great disturbance in the crypto: Understanding cryptocurrency returns under attacks","volume":"2","author":"Ramos","year":"2021","journal-title":"Blockchain Res. Appl."},{"key":"ref_11","unstructured":"Bernauer, A., Faro, S., H\u00e4mmerle, R., Huschenbett, M., Kiefer, M., Lochbihler, A., M\u00e4ki, J., Mazzoli, F., Meier, S., and Mitchell, N. (2023). Daml: A smart contract language for securely automating real-world multi-party business workflows. arXiv."},{"key":"ref_12","doi-asserted-by":"crossref","unstructured":"Al-Azzoni, I., and Iqbal, S. (2024). Access Control Verification in Smart Contracts Using Colored Petri Nets. Computers, 13.","DOI":"10.3390\/computers13110274"},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"(2022). Information Security, Cybersecurity and Privacy Protection\u2014Information Security Management Systems\u2014Requirements (Standard No. ISO\/IEC 27001:2022). Available online: https:\/\/www.iso.org\/standard\/27001.","DOI":"10.2307\/j.ctv30qq13d"},{"key":"ref_14","unstructured":"American Institute of Certified Public Accountants (2025, May 30). 2017 Trust Services Criteria for Security, Availability, Processing Integrity, Confidentiality, and Privacy (With Revised Points of Focus\u20142022). Available online: https:\/\/www.aicpa-cima.com\/resources\/download\/2017-trust-services-criteria-with-revised-points-of-focus-2022."},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"National Institute of Standards and Technology (2025, May 30). Security and Privacy Controls for Information Systems and Organizations, Available online: https:\/\/doi.org\/10.6028\/NIST.SP.800-53r5.","DOI":"10.6028\/NIST.SP.800-53r5"},{"key":"ref_16","first-page":"1","article-title":"Auditing with Smart Contracts","volume":"18","author":"Rozario","year":"2018","journal-title":"Int. J. Digit. Account. Res."},{"key":"ref_17","doi-asserted-by":"crossref","unstructured":"Malatji, M. (2023, January 26\u201327). Management of enterprise cyber security: A review of ISO\/IEC 27001: 2022. Proceedings of the 2023 International Conference on Cyber Management and Engineering (CyMaEn), Bangkok, Thailand.","DOI":"10.1109\/CyMaEn57228.2023.10051114"},{"key":"ref_18","unstructured":"Nakamoto, S. (2025, May 30). Bitcoin: A Peer-to-Peer Electronic Cash System. Available online: https:\/\/assets.pubpub.org\/d8wct41f\/31611263538139.pdf."},{"key":"ref_19","unstructured":"Buterin, V. (2025, May 30). A Next-Generation Smart Contract and Decentralized Application Platform. White Paper. Available online: https:\/\/blockchainlab.com\/pdf\/Ethereum_white_paper-a_next_generation_smart_contract_and_decentralized_application_platform-vitalik-buterin.pdf."},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Atzei, N., Bartoletti, M., and Cimoli, T. (2017, January 22\u201329). A survey of attacks on ethereum smart contracts (sok). Proceedings of the Principles of Security and Trust: 6th International Conference, POST 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden.","DOI":"10.1007\/978-3-662-54455-6_8"},{"key":"ref_21","doi-asserted-by":"crossref","unstructured":"Nikoli\u0107, I., Kolluri, A., Sergey, I., Saxena, P., and Hobor, A. (2018, January 3\u20137). Finding the greedy, prodigal, and suicidal contracts at scale. Proceedings of the 34th Annual Computer Security Applications Conference, San Juan, PR, USA.","DOI":"10.1145\/3274694.3274743"},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Luu, L., Chu, D.H., Olickel, H., Saxena, P., and Hobor, A. (2016, January 24\u201328). Making smart contracts smarter. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria.","DOI":"10.1145\/2976749.2978309"},{"key":"ref_23","doi-asserted-by":"crossref","unstructured":"Androulaki, E., Barger, A., Bortnikov, V., Cachin, C., Christidis, K., De Caro, A., Enyeart, D., Ferris, C., Laventman, G., and Manevich, Y. (2018, January 23\u201326). Hyperledger fabric: A distributed operating system for permissioned blockchains. Proceedings of the Thirteenth EuroSys Conference, Porto, Portugal.","DOI":"10.1145\/3190508.3190538"},{"key":"ref_24","doi-asserted-by":"crossref","unstructured":"Kiayias, A., Russell, A., David, B., and Oliynykov, R. (2017, January 20\u201324). Ouroboros: A provably secure proof-of-stake blockchain protocol. Proceedings of the 37th International Cryptology Conference, Santa Barbara, CA, USA.","DOI":"10.1007\/978-3-319-63688-7_12"},{"key":"ref_25","unstructured":"Cardano Documentation (2025, May 12). Plutus Smart Contracts. Available online: https:\/\/docs.cardano.org\/developer-resources\/smart-contracts\/plutus."},{"key":"ref_26","first-page":"1","article-title":"Procedures for performing systematic reviews","volume":"33","author":"Kitchenham","year":"2004","journal-title":"Keele UK Keele Univ."},{"key":"ref_27","doi-asserted-by":"crossref","first-page":"77894","DOI":"10.1109\/ACCESS.2019.2921624","article-title":"A survey on security verification of blockchain smart contracts","volume":"7","author":"Liu","year":"2019","journal-title":"IEEE Access"},{"key":"ref_28","unstructured":"Praitheeshan, P., Pan, L., Yu, J., Liu, J., and Doss, R. (2019). Security analysis methods on Ethereum smart contract vulnerabilities: A survey. arXiv."},{"key":"ref_29","doi-asserted-by":"crossref","first-page":"50759","DOI":"10.1109\/ACCESS.2019.2911031","article-title":"Security, performance, and applications of smart contracts: A systematic survey","volume":"7","author":"Rouhani","year":"2019","journal-title":"IEEE Access"},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Murray, Y., and Anisi, D.A. (2019, January 24\u201326). Survey of formal verification methods for smart contracts on blockchain. Proceedings of the 2019 10th IFIP International Conference on New Technologies, Mobility and Security (NTMS), Canary Island, Spain.","DOI":"10.1109\/NTMS.2019.8763832"},{"key":"ref_31","doi-asserted-by":"crossref","unstructured":"Di Angelo, M., and Salzer, G. (2019, January 4\u20139). A survey of tools for analyzing ethereum smart contracts. Proceedings of the 2019 IEEE International Conference on Decentralized Applications and Infrastructures (DAPPCON), Newark, CA, USA.","DOI":"10.1109\/DAPPCON.2019.00018"},{"key":"ref_32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3464421","article-title":"A survey of smart contract formal specification and verification","volume":"54","author":"Tolmach","year":"2021","journal-title":"ACM Comput. Surv."},{"key":"ref_33","doi-asserted-by":"crossref","unstructured":"Hu, B., Zhang, Z., Liu, J., Liu, Y., Yin, J., Lu, R., and Lin, X. (2020). A Comprehensive Survey on Smart Contract Construction and Execution: Paradigms, Tools and Systems. arXiv.","DOI":"10.1016\/j.patter.2020.100179"},{"key":"ref_34","unstructured":"Imeri, A., Agoulmine, N., and Khadraoui, D. (2020, January 27\u201329). Smart Contract modeling and verification techniques: A survey. Proceedings of the 8th International Workshop on ADVANCEs in ICT Infrastructures and Services, Cancun, Mexico."},{"key":"ref_35","doi-asserted-by":"crossref","unstructured":"Wang, Z., Jin, H., Dai, W., Choo, K.K.R., and Zou, D. (2020). Ethereum smart contract security research: Survey and future research opportunities. Front. Comput. Sci., 15.","DOI":"10.1007\/s11704-020-9284-9"},{"key":"ref_36","doi-asserted-by":"crossref","first-page":"101227","DOI":"10.1016\/j.pmcj.2020.101227","article-title":"Verification of smart contracts: A survey","volume":"67","author":"Almakhour","year":"2020","journal-title":"Pervasive Mob. Comput."},{"key":"ref_37","unstructured":"Munir, S., and Taha, W. (2023). Pre-deployment Analysis of Smart Contracts\u2014A Survey. arXiv."},{"key":"ref_38","unstructured":"Qian, P., Liu, Z., He, Q., Huang, B., Tian, D., and Wang, X. (2022). Smart contract vulnerability detection technique: A survey. arXiv."},{"key":"ref_39","doi-asserted-by":"crossref","first-page":"6605","DOI":"10.1109\/ACCESS.2021.3140091","article-title":"Systematic review of security vulnerabilities in ethereum blockchain smart contract","volume":"10","author":"Kushwaha","year":"2022","journal-title":"IEEE Access"},{"key":"ref_40","doi-asserted-by":"crossref","first-page":"57037","DOI":"10.1109\/ACCESS.2022.3169902","article-title":"Ethereum smart contract analysis tools: A systematic review","volume":"10","author":"Kushwaha","year":"2022","journal-title":"IEEE Access"},{"key":"ref_41","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1002\/spe.3156","article-title":"Detecting functional and security-related issues in smart contracts: A systematic literature review","volume":"53","author":"Piantadosi","year":"2023","journal-title":"Softw. Pract. Exp."},{"key":"ref_42","doi-asserted-by":"crossref","unstructured":"Rameder, H., Di Angelo, M., and Salzer, G. (2022). Review of automated vulnerability analysis of smart contracts on Ethereum. Front. Blockchain, 5.","DOI":"10.3389\/fbloc.2022.814977"},{"key":"ref_43","doi-asserted-by":"crossref","first-page":"358","DOI":"10.3390\/jcp2020019","article-title":"The state of ethereum smart contracts security: Vulnerabilities, countermeasures, and tool support","volume":"2","author":"Zhou","year":"2022","journal-title":"J. Cybersecur. Priv."},{"key":"ref_44","first-page":"134","article-title":"Security Strengths and Weaknesses of Blockchain Smart Contract System: A Survey","volume":"16","author":"Ndiaye","year":"2022","journal-title":"Int. J. Inf. Commun. Eng."},{"key":"ref_45","doi-asserted-by":"crossref","first-page":"100492","DOI":"10.1016\/j.cosrev.2022.100492","article-title":"Blockchain verification and validation: Techniques, challenges, and research directions","volume":"45","author":"Marijan","year":"2022","journal-title":"Comput. Sci. Rev."},{"key":"ref_46","doi-asserted-by":"crossref","first-page":"150184","DOI":"10.1109\/ACCESS.2019.2946988","article-title":"Smart contract security: A software lifecycle perspective","volume":"7","author":"Huang","year":"2019","journal-title":"IEEE Access"},{"key":"ref_47","doi-asserted-by":"crossref","first-page":"24416","DOI":"10.1109\/ACCESS.2020.2970495","article-title":"Smart contract: Attacks and protections","volume":"8","author":"Sayeed","year":"2020","journal-title":"IEEE Access"},{"key":"ref_48","doi-asserted-by":"crossref","unstructured":"Tang, X., Zhou, K., Cheng, J., Li, H., and Yuan, Y. (2021, January 19\u201323). The vulnerabilities in smart contracts: A survey. Proceedings of the Advances in Artificial Intelligence and Security: 7th International Conference, ICAIS 2021, Dublin, Ireland.","DOI":"10.1007\/978-3-030-78621-2_14"},{"key":"ref_49","first-page":"1","article-title":"A survey on ethereum systems security: Vulnerabilities, attacks, and defenses","volume":"53","author":"Chen","year":"2020","journal-title":"ACM Comput. Surv."},{"key":"ref_50","doi-asserted-by":"crossref","first-page":"110891","DOI":"10.1016\/j.jss.2020.110891","article-title":"A systematic literature review of blockchain and smart contract development: Techniques, tools, and open challenges","volume":"174","author":"Vacca","year":"2021","journal-title":"J. Syst. Softw."},{"key":"ref_51","doi-asserted-by":"crossref","unstructured":"Fekih, R.B., Lahami, M., Jmaiel, M., and Bradai, S. (2023, January 14\u201316). Formal Verification of Smart Contracts Based on Model Checking: An Overview. Proceedings of the 2023 IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE), Paris, France.","DOI":"10.1109\/WETICE57085.2023.10477834"},{"key":"ref_52","doi-asserted-by":"crossref","first-page":"70870","DOI":"10.1109\/ACCESS.2024.3401623","article-title":"A Survey of Vulnerability Detection Techniques by Smart Contract Tools","volume":"12","author":"Khan","year":"2024","journal-title":"IEEE Access"},{"key":"ref_53","doi-asserted-by":"crossref","first-page":"4522","DOI":"10.1109\/TSC.2024.3463394","article-title":"A Survey on Security Analysis Methods of Smart Contracts","volume":"17","author":"Zhu","year":"2024","journal-title":"IEEE Trans. Serv. Comput."},{"key":"ref_54","doi-asserted-by":"crossref","unstructured":"Deng, Y., Wang, L., Wang, L., Li, J., and Yong, Q. (2023, January 18\u201321). A Survey on Automatic Discover Approach by Using Static Analysis for Smart Contract Vulnerability. Proceedings of the 2023 International Conference on Networking and Network Applications (NaNA), Qingdao, China.","DOI":"10.1109\/NaNA60121.2023.00035"},{"key":"ref_55","doi-asserted-by":"crossref","first-page":"112160","DOI":"10.1016\/j.jss.2024.112160","article-title":"Vulnerability detection techniques for smart contracts: A systematic literature review","volume":"217","author":"Vidal","year":"2024","journal-title":"J. Syst. Softw."},{"key":"ref_56","first-page":"1","article-title":"A Review of Deep Learning-Based Vulnerability Detection Tools for Ethernet Smart Contracts","volume":"140","author":"Wu","year":"2024","journal-title":"CMES-Comput. Model. Eng. Sci."},{"key":"ref_57","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1007\/s10009-024-00758-x","article-title":"Software verification challenges in the blockchain ecosystem","volume":"26","author":"Olivieri","year":"2024","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_58","doi-asserted-by":"crossref","first-page":"7111","DOI":"10.1007\/s10586-024-04421-7","article-title":"A systematic mapping on software testing for blockchains","volume":"27","author":"Kalkan","year":"2024","journal-title":"Clust. Comput."},{"key":"ref_59","doi-asserted-by":"crossref","unstructured":"Garfatta, I., Klai, K., Gaaloul, W., and Graiet, M. (2021, January 1\u20135). A Survey on Formal Verification for Solidity Smart Contracts. Proceedings of the 2021 Australasian Computer Science Week Multiconference, Dunedin, New Zealand.","DOI":"10.1145\/3437378.3437879"},{"key":"ref_60","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3643895","article-title":"A survey of ethereum smart contract security: Attacks and detection","volume":"3","author":"Jiao","year":"2024","journal-title":"Distrib. Ledger Technol. Res. Pract."},{"key":"ref_61","doi-asserted-by":"crossref","unstructured":"Cousot, P., and Cousot, R. (1977, January 17\u201319). Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, Los Angeles, CA, USA.","DOI":"10.1145\/512950.512973"},{"key":"ref_62","doi-asserted-by":"crossref","unstructured":"Tsankov, P., Dan, A., Drachsler-Cohen, D., Gervais, A., Buenzli, F., and Vechev, M. (2018, January 15\u201319). Securify: Practical security analysis of smart contracts. Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, Toronto, ON, Canada.","DOI":"10.1145\/3243734.3243780"},{"key":"ref_63","doi-asserted-by":"crossref","first-page":"111653","DOI":"10.1016\/j.jss.2023.111653","article-title":"Enhancing Ethereum smart-contracts static analysis by computing a precise Control-Flow Graph of Ethereum bytecode","volume":"200","author":"Pasqua","year":"2023","journal-title":"J. Syst. Softw."},{"key":"ref_64","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1145\/360248.360252","article-title":"Symbolic execution and program testing","volume":"19","author":"King","year":"1976","journal-title":"Commun. ACM"},{"key":"ref_65","doi-asserted-by":"crossref","unstructured":"Feist, J., Mounier, L., Bardin, S., David, R., and Potet, M.L. (2016, January 5\u20136). Finding the needle in the heap: Combining static analysis and dynamic symbolic execution to trigger use-after-free. Proceedings of the 6th Workshop on Software Security, Protection, and Reverse Engineering, Los Angeles, CA, USA.","DOI":"10.1145\/3015135.3015137"},{"key":"ref_66","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1145\/1543135.1542486","article-title":"TAJ: Effective taint analysis of web applications","volume":"44","author":"Tripp","year":"2009","journal-title":"ACM Sigplan Not."},{"key":"ref_67","doi-asserted-by":"crossref","unstructured":"Bose, P., Das, D., Chen, Y., Feng, Y., Kruegel, C., and Vigna, G. (2022, January 23\u201325). Sailfish: Vetting smart contract state-inconsistency bugs in seconds. Proceedings of the 2022 IEEE Symposium on Security and Privacy (SP), San Francisco, CA, USA.","DOI":"10.1109\/SP46214.2022.9833721"},{"key":"ref_68","doi-asserted-by":"crossref","unstructured":"Sen, K. (2007, January 5\u20139). Concolic testing. Proceedings of the 22nd IEEE\/ACM International Conference on Automated Software Engineering, Atlanta, GA, USA.","DOI":"10.1145\/1321631.1321746"},{"key":"ref_69","unstructured":"Wang, S.J., Yao, J., Pei, K., Takahashi, H., and Yang, J. (2024). Detecting Buggy Contracts via Smart Testing. arXiv."},{"key":"ref_70","unstructured":"Sutton, M., Greene, A., and Amini, P. (2007). Fuzzing: Brute Force Vulnerability Discovery, Pearson Education."},{"key":"ref_71","unstructured":"Shou, C., Liu, J., Lu, D., and Sen, K. (2024). Llm4fuzz: Guided fuzzing of smart contracts with large language models. arXiv."},{"key":"ref_72","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1109\/C-M.1978.218136","article-title":"Hints on test data selection: Help for the practicing programmer","volume":"11","author":"DeMillo","year":"1978","journal-title":"Computer"},{"key":"ref_73","doi-asserted-by":"crossref","unstructured":"Petrovi\u0107, G., Ivankovi\u0107, M., Fraser, G., and Just, R. (2021, January 25\u201328). Does mutation testing improve testing practices?. Proceedings of the 2021 IEEE\/ACM 43rd International Conference on Software Engineering (ICSE), Madrid, Spain.","DOI":"10.1109\/ICSE43902.2021.00087"},{"key":"ref_74","doi-asserted-by":"crossref","unstructured":"Liu, Y., Li, Y., Lin, S.W., and Yan, Q. (2020, January 8\u201313). ModCon: A model-based testing platform for smart contracts. Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Virtual Event.","DOI":"10.1145\/3368089.3417939"},{"key":"ref_75","unstructured":"Suvorov, D., and Ulyantsev, V. (2019). Smart contract design meets state machine synthesis: Case studies. arXiv."},{"key":"ref_76","doi-asserted-by":"crossref","unstructured":"Liu, S., Xu, Y., Yang, X., Hui, B., and Hu, F. (2024). Variable-State-Trigger: A Formal Model of Smart Contracts Based on Conditional Response and Finite State Automata and Its Application. Electronics, 13.","DOI":"10.3390\/electronics13234680"},{"key":"ref_77","doi-asserted-by":"crossref","unstructured":"Xu, H., Fan, J., and Han, L. (2024, January 3\u20135). Smart contract vulnerability detection based on adaptive genetic algorithm. Proceedings of the Fourth International Conference on Applied Mathematics, Modelling, and Intelligent Computing (CAMMIC 2024), Kaifeng, China.","DOI":"10.1117\/12.3036907"},{"key":"ref_78","unstructured":"Driessen, S., Di Nucci, D., Monsieur, G., Tamburri, D.A., and Heuvel, W.J.v.d. (2021). Automated test-case generation for solidity smart contracts: The AGSolT approach and its evaluation. arXiv."},{"key":"ref_79","doi-asserted-by":"crossref","first-page":"859","DOI":"10.1145\/355604.361591","article-title":"The humble programmer","volume":"15","author":"Dijkstra","year":"1972","journal-title":"Commun. ACM"},{"key":"ref_80","doi-asserted-by":"crossref","unstructured":"Matsuo, S. (2017, January 2\u20136). How formal analysis and verification add security to blockchain-based systems. Proceedings of the 2017 Formal Methods in Computer Aided Design (FMCAD), Vienna, Austria.","DOI":"10.23919\/FMCAD.2017.8102228"},{"key":"ref_81","unstructured":"Mavridou, A., and Laszka, A. (2018, January 14\u201320). Tool demonstration: Fsolidm for designing secure ethereum smart contracts. Proceedings of the Principles of Security and Trust: 7th International Conference, POST 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece."},{"key":"ref_82","doi-asserted-by":"crossref","unstructured":"Mavridou, A., Laszka, A., Stachtiari, E., and Dubey, A. (2019, January 18\u201322). VeriSolid: Correct-by-design smart contracts for Ethereum. Proceedings of the Financial Cryptography and Data Security: 23rd International Conference, FC 2019, Frigate Bay, St. Kitts and Nevis. Revised Selected Papers 23.","DOI":"10.1007\/978-3-030-32101-7_27"},{"key":"ref_83","doi-asserted-by":"crossref","unstructured":"Neha\u00ef, Z., and Bobot, F. (2019, January 7\u201311). Deductive proof of industrial smart contracts using Why3. Proceedings of the Formal Methods. FM 2019 International Workshops, Porto, Portugal. Revised Selected Papers, Part I 3.","DOI":"10.1007\/978-3-030-54994-7_22"},{"key":"ref_84","doi-asserted-by":"crossref","unstructured":"Bao, T., and Liu, Y. (2021, January 20\u201322). A privacy-preserving framework for smart contracts based on stochastic model checking. Proceedings of the 2021 IEEE 20th International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom), Shenyang, China.","DOI":"10.1109\/TrustCom53373.2021.00075"},{"key":"ref_85","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1109\/MIS.2020.2977594","article-title":"Formal analysis of smart contract based on colored petri nets","volume":"35","author":"Duo","year":"2020","journal-title":"IEEE Intell. Syst."},{"key":"ref_86","doi-asserted-by":"crossref","unstructured":"Amani, S., B\u00e9gel, M., Bortin, M., and Staples, M. (2018, January 8\u20139). Towards verifying ethereum smart contract bytecode in Isabelle\/HOL. Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Los Angeles, CA, USA.","DOI":"10.1145\/3167084"},{"key":"ref_87","doi-asserted-by":"crossref","unstructured":"Annenkov, D., and Spitters, B. (2019). Towards a smart contract verification framework in Coq. arXiv.","DOI":"10.1145\/3372885.3373829"},{"key":"ref_88","unstructured":"Hirai, Y. (2024, September 20). eth-isabelle: Formalising the Ethereum Virtual Machine in Isabelle\/HOL. Available online: https:\/\/github.com\/pirapira\/eth-isabelle."},{"key":"ref_89","doi-asserted-by":"crossref","unstructured":"Emerson, E.A. (2008). The beginning of model checking: A personal perspective. 25 Years of Model Checking, Springer.","DOI":"10.1007\/978-3-540-69850-0_2"},{"key":"ref_90","unstructured":"Baier, C., and Katoen, J.P. (2008). Principles of Model Checking, MIT Press."},{"key":"ref_91","unstructured":"Mavridis, A. (2024, February 08). FSolidM\/VeriSolid Framework. Available online: https:\/\/github.com\/anmavrid\/smart-contracts."},{"key":"ref_92","doi-asserted-by":"crossref","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., and Tonetta, S. (2014, January 18\u201322). The nuXmv symbolic model checker. Proceedings of the Computer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria.","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"ref_93","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/s100090050046","article-title":"NuSMV: A new symbolic model checker","volume":"2","author":"Cimatti","year":"2000","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"ref_94","doi-asserted-by":"crossref","unstructured":"Nehai, Z., Piriou, P.Y., and Daumas, F. (August, January 30). Model-checking of smart contracts. Proceedings of the 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), Halifax, NS, Canada.","DOI":"10.1109\/Cybermatics_2018.2018.00185"},{"key":"ref_95","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/j.icte.2019.07.002","article-title":"Policy specification and verification for blockchain and smart contracts in 5G networks","volume":"6","author":"Unal","year":"2020","journal-title":"ICT Express"},{"key":"ref_96","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., and Parker, D. (2002, January 14\u201317). PRISM: Probabilistic symbolic model checker. Proceedings of the 12th International Conference on Modelling Techniques and Tools for Computer Performance Evaluation, London, UK.","DOI":"10.1007\/3-540-46029-2_13"},{"key":"ref_97","unstructured":"Mazurek, L. (2024, February 24). ethver: Ethereum Smart Contract Versioning Tool. Available online: https:\/\/github.com\/lukmaz\/ethver."},{"key":"ref_98","doi-asserted-by":"crossref","unstructured":"Mazurek, \u0141. (2021, January 5). EthVer: Formal verification of randomized Ethereum smart contracts. Proceedings of the Financial Cryptography and Data Security. FC 2021 International Workshops: CoDecFin, DeFi, VOTING, and WTSC, Virtual Event. Revised Selected Papers 25.","DOI":"10.1007\/978-3-662-63958-0_30"},{"key":"ref_99","unstructured":"Microsoft (2024, February 25). VeriSol: Formal Verification for Solidity Smart Contracts. Available online: https:\/\/github.com\/microsoft\/verisol."},{"key":"ref_100","unstructured":"Wang, Y., Lahiri, S.K., Chen, S., Pan, R., Dillig, I., Born, C., and Naseer, I. (2018). Formal specification and verification of smart contracts for Azure blockchain. arXiv."},{"key":"ref_101","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S., and Lahiri, S.K. (2012, January 7\u201313). A solver for reachability modulo theories. Proceedings of the Computer Aided Verification: 24th International Conference, CAV 2012, Berkeley, CA, USA.","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"ref_102","unstructured":"Ben-Ari, M. (2008). Principles of the Spin Model Checker, Springer Science & Business Media."},{"key":"ref_103","doi-asserted-by":"crossref","unstructured":"Bai, X., Cheng, Z., Duan, Z., and Hu, K. (2018, January 8\u201310). Formal modeling and verification of smart contracts. Proceedings of the 2018 7th International Conference on Software and Computer Applications, Kuantan, Malaysia.","DOI":"10.1145\/3185089.3185138"},{"key":"ref_104","doi-asserted-by":"crossref","unstructured":"Yang, Z., Dai, M., and Guo, J. (2022). Formal modeling and verification of smart contracts with SPIN. Electronics, 11.","DOI":"10.3390\/electronics11193091"},{"key":"ref_105","doi-asserted-by":"crossref","first-page":"101129","DOI":"10.1016\/j.pmcj.2020.101129","article-title":"Model checking smart contracts for ethereum","volume":"63","author":"Osterland","year":"2020","journal-title":"Pervasive Mob. Comput."},{"key":"ref_106","doi-asserted-by":"crossref","unstructured":"Liu, Z., and Liu, J. (2019, January 15\u201319). Formal verification of blockchain smart contract based on colored petri net models. Proceedings of the 2019 IEEE 43rd Annual Computer Software and Applications Conference (COMPSAC), Milwaukee, WI, USA.","DOI":"10.1109\/COMPSAC.2019.10265"},{"key":"ref_107","doi-asserted-by":"crossref","unstructured":"He, Y., Dong, H., Wang, R., and Wu, H. (2022, January 9\u201311). Formal Verification of Smart Contract Based on Timed Colored Petri Net. Proceedings of the 2022 11th International Conference on Networks, Communication and Computing, Beijing, China.","DOI":"10.1145\/3579895.3579943"},{"key":"ref_108","doi-asserted-by":"crossref","unstructured":"Abdellatif, T., and Brousmiche, K.L. (2018, January 26\u201328). Formal verification of smart contracts based on users and blockchain behaviors models. Proceedings of the 2018 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS), Paris, France.","DOI":"10.1109\/NTMS.2018.8328737"},{"key":"ref_109","unstructured":"Basu, A., Bozga, M., and Sifakis, J. (2006, January 11\u201315). Modeling heterogeneous real-time components in BIP. Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM\u201906), Pune, India."},{"key":"ref_110","doi-asserted-by":"crossref","first-page":"012152","DOI":"10.1088\/1757-899X\/734\/1\/012152","article-title":"Statistical model checking for blockchain-based applications","volume":"Volume 734","author":"Maksimov","year":"2020","journal-title":"Proceedings of the IOP Conference Series: Materials Science and Engineering"},{"key":"ref_111","doi-asserted-by":"crossref","first-page":"8151","DOI":"10.1109\/ACCESS.2022.3143145","article-title":"Formal verification of blockchain smart contracts via atl model checking","volume":"10","author":"Nam","year":"2022","journal-title":"IEEE Access"},{"key":"ref_112","unstructured":"Lomuscio, A., and Raimondi, F. (April, January 25). MCMAS: A model checker for multi-agent systems. Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Vienna, Austria."},{"key":"ref_113","doi-asserted-by":"crossref","unstructured":"van der Meyden, R. (2019, January 14\u201317). On the specification and verification of atomic swap smart contracts. Proceedings of the 2019 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), Seoul, Republic of Korea.","DOI":"10.1109\/BLOC.2019.8751250"},{"key":"ref_114","doi-asserted-by":"crossref","unstructured":"Gammie, P., and Van Der Meyden, R. (2004, January 13\u201317). MCK: Model checking the logic of knowledge. Proceedings of the Computer Aided Verification: 16th International Conference, CAV 2004, Boston, MA, USA.","DOI":"10.1007\/978-3-540-27813-9_41"},{"key":"ref_115","doi-asserted-by":"crossref","unstructured":"Qu, M., Huang, X., Chen, X., Wang, Y., Ma, X., and Liu, D. (2018, January 10\u201312). Formal verification of smart contracts from the perspective of concurrency. Proceedings of the Smart Blockchain: First International Conference, SmartBlock 2018, Tokyo, Japan.","DOI":"10.1007\/978-3-030-05764-0_4"},{"key":"ref_116","unstructured":"FDR2 User Manual (2025, May 30). Failures-Divergence Refinement. Available online: http:\/\/www.cs.ox.ac.uk\/projects\/concurrency-tools\/download\/fdr2manual-2.94.pdf."},{"key":"ref_117","doi-asserted-by":"crossref","unstructured":"Annenkov, D., Milo, M., Nielsen, J.B., and Spitters, B. (2021, January 17\u201319). Extracting Smart Contracts Tested and Verified in Coq. Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, New York, NY, USA.","DOI":"10.1145\/3437992.3439934"},{"key":"ref_118","doi-asserted-by":"crossref","first-page":"21411","DOI":"10.1109\/ACCESS.2020.2969437","article-title":"A hybrid formal verification system in coq for ensuring the reliability and security of ethereum-based service smart contracts","volume":"8","author":"Yang","year":"2020","journal-title":"IEEE Access"},{"key":"ref_119","doi-asserted-by":"crossref","first-page":"37770","DOI":"10.1109\/ACCESS.2019.2905428","article-title":"Fether: An extensible definitional interpreter for smart-contract verifications in coq","volume":"7","author":"Yang","year":"2019","journal-title":"IEEE Access"},{"key":"ref_120","doi-asserted-by":"crossref","unstructured":"Zhu, J., Hu, K., Filali, M., Bodeveix, J.P., Talpin, J.P., and Cao, H. (2021, January 12\u201316). Formal simulation and verification of solidity contracts in event-b. Proceedings of the 2021 IEEE 45th Annual Computers, Software, and Applications Conference (COMPSAC), Madrid, Spain.","DOI":"10.1109\/COMPSAC51774.2021.00183"},{"key":"ref_121","doi-asserted-by":"crossref","unstructured":"Jiao, J., Lin, S.W., and Sun, J. (2020, January 25\u201330). A Generalized Formal Semantic Framework for Smart Contracts. Proceedings of the Fundamental Approaches to Software Engineering (FASE), Dublin, Ireland.","DOI":"10.1007\/978-3-030-45234-6_4"},{"key":"ref_122","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3498665","article-title":"SolType: Refinement types for arithmetic overflow in solidity","volume":"6","author":"Tan","year":"2022","journal-title":"Proc. ACM Program. Lang."},{"key":"ref_123","doi-asserted-by":"crossref","unstructured":"Jiang, F., Chao, K., Xiao, J., Liu, Q., Gu, K., Wu, J., and Cao, Y. (2023). Enhancing smart-contract security through machine learning: A survey of approaches and techniques. Electronics, 12.","DOI":"10.3390\/electronics12092046"},{"key":"ref_124","unstructured":"Leroy, X., Blazy, S., K\u00e4stner, D., Schommer, B., Pister, M., and Ferdinand, C. (2016, January 27\u201329). CompCert-a formally verified optimizing compiler. Proceedings of the ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, Toulouse, France."},{"key":"ref_125","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/s00165-016-0354-6","article-title":"Correct-by-construction model driven engineering composition operators","volume":"28","author":"Pantel","year":"2016","journal-title":"Form. Asp. Comput."},{"key":"ref_126","doi-asserted-by":"crossref","unstructured":"Nielsen, E.H., Annenkov, D., and Spitters, B. (2023, January 16\u201317). Formalising decentralised exchanges in Coq. Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Boston, MA, USA.","DOI":"10.1145\/3573105.3575685"},{"key":"ref_127","unstructured":"Ethereum Foundation (2024, February 08). Remix IDE: Ethereum Smart Contract Development Environment. Available online: https:\/\/github.com\/ethereum\/remix-ide."},{"key":"ref_128","unstructured":"Tikhomirov, S., Voskresenskaya, E., Ivanitskiy, I., Takhaviev, R., Marchenko, E., and Alexandrov, Y. (June, January 27). Smartcheck: Static analysis of ethereum smart contracts. Proceedings of the 1st International Workshop on Emerging Trends in Software Engineering for Blockchain, Gothia, Sweden."},{"key":"ref_129","unstructured":"Palkeo (2024, February 24). Pakala: Yet Another EVM Symbolic Execution Tool. Available online: https:\/\/www.palkeo.com\/en\/projets\/ethereum\/pakala.html."},{"key":"ref_130","doi-asserted-by":"crossref","unstructured":"Grieco, G., Song, W., Cygan, A., Feist, J., and Groce, A. (2020, January 18\u201322). Echidna: Effective, usable, and fast fuzzing for smart contracts. Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event.","DOI":"10.1145\/3395363.3404366"},{"key":"ref_131","doi-asserted-by":"crossref","unstructured":"Groce, A., and Grieco, G. (2021, January 11\u201317). Echidna-parade: A tool for diverse multicore smart contract fuzzing. Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, Aarhus, Denmark.","DOI":"10.1145\/3460319.3469076"},{"key":"ref_132","doi-asserted-by":"crossref","unstructured":"Nassirzadeh, B., Sun, H., Banescu, S., and Ganesh, V. (2022, January 12\u201314). Gas gauge: A security analysis tool for smart contract out-of-gas vulnerabilities. Proceedings of the International Conference on Mathematical Research for Blockchain Economy, Vilamoura, Portugal.","DOI":"10.1007\/978-3-031-18679-0_9"},{"key":"ref_133","doi-asserted-by":"crossref","unstructured":"Li, Z., Wu, H., Xu, J., Wang, X., Zhang, L., and Chen, Z. (2019, January 10\u201315). Musc: A tool for mutation testing of ethereum smart contract. Proceedings of the 2019 34th IEEE\/ACM International Conference on Automated Software Engineering (ASE), San Diego, CA, USA.","DOI":"10.1109\/ASE.2019.00136"},{"key":"ref_134","doi-asserted-by":"crossref","unstructured":"Peng, C., Akca, S., and Rajan, A. (2019, January 2\u20135). SIF: A framework for solidity contract instrumentation and analysis. Proceedings of the 2019 26th Asia-Pacific Software Engineering Conference (APSEC), Putrajava, Malaysia.","DOI":"10.1109\/APSEC48747.2019.00069"},{"key":"ref_135","doi-asserted-by":"crossref","unstructured":"Feist, J., Grieco, G., and Groce, A. (2019, January 17). Slither: A static analysis framework for smart contracts. Proceedings of the 2019 IEEE\/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), Montreal, QC, Canada.","DOI":"10.1109\/WETSEB.2019.00008"},{"key":"ref_136","unstructured":"Hajdu, \u00c1., and Jovanovi\u0107, D. (2019, January 13\u201314). solc-verify: A modular verifier for solidity smart contracts. Proceedings of the Verified Software. Theories, Tools, and Experiments: 11th International Conference, VSTTE 2019, New York City, NY, USA. Revised Selected Papers 11."},{"key":"ref_137","unstructured":"Protofire (2024, February 25). Solhint: Solidity Linter. Available online: https:\/\/protofire.github.io\/solhint\/."},{"key":"ref_138","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1016\/j.ins.2021.08.007","article-title":"SolGuard: Preventing external call issues in smart contract-based multi-agent robotic systems","volume":"579","author":"Praitheeshan","year":"2021","journal-title":"Inf. Sci."},{"key":"ref_139","unstructured":"Zhang, P., Xiao, F., and Luo, X. (2019). Soliditycheck: Quickly detecting smart contract problems through regular expressions. arXiv."},{"key":"ref_140","doi-asserted-by":"crossref","unstructured":"Honig, J.J., Everts, M.H., and Huisman, M. (2019, January 26\u201327). Practical mutation testing for smart contracts. Proceedings of the International Workshop on Data Privacy Management, International Workshop on Cryptocurrencies and Blockchain Technology, Luxembourg.","DOI":"10.1007\/978-3-030-31500-9_19"},{"key":"ref_141","unstructured":"Frank, J., Aschermann, C., and Holz, T. (2020, January 12\u201314). ETHBMC: A bounded model checker for smart contracts. Proceedings of the 29th USENIX Security Symposium (USENIX Security 20), Boston, MA, USA."},{"key":"ref_142","unstructured":"Revere, R. (2024, February 13). solgraph: Visualize Solidity Control Flow for Smart Contracts. Available online: https:\/\/github.com\/raineorshine\/solgraph."},{"key":"ref_143","doi-asserted-by":"crossref","unstructured":"Kolluri, A., Nikolic, I., Sergey, I., Hobor, A., and Saxena, P. (2019, January 15\u201319). Exploiting the laws of order in smart contracts. Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, Beijing, China.","DOI":"10.1145\/3293882.3330560"},{"key":"ref_144","unstructured":"Veloso, N. (2024, February 26). Conkas: Ethereum Smart Contract Security Analysis. Available online: https:\/\/github.com\/nveloso\/conkas."},{"key":"ref_145","doi-asserted-by":"crossref","first-page":"2189","DOI":"10.1109\/TSE.2021.3054928","article-title":"Defectchecker: Automated smart contract defect detection by analyzing evm bytecode","volume":"48","author":"Chen","year":"2021","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_146","doi-asserted-by":"crossref","unstructured":"Norvill, R., Pontiveros, B.B.F., State, R., and Cullen, A. (2018, January 23\u201327). Visual emulation for Ethereum\u2019s virtual machine. Proceedings of the NOMS 2018\u20142018 IEEE\/IFIP Network Operations and Management Symposium, Taipei, Taiwan.","DOI":"10.1109\/NOMS.2018.8406332"},{"key":"ref_147","unstructured":"Grishchenko, I., Maffei, M., and Schneidewind, C. (2018). Ethertrust: Sound static analysis of ethereum bytecode. Tech. Univ. Wien Tech. Rep., 1\u201341. Available online: https:\/\/www.netidee.at\/sites\/default\/files\/2018-07\/staticanalysis.pdf."},{"key":"ref_148","doi-asserted-by":"crossref","unstructured":"Albert, E., Gordillo, P., Livshits, B., Rubio, A., and Sergey, I. (2018, January 7\u201310). Ethir: A framework for high-level analysis of ethereum bytecode. Proceedings of the International Symposium on Automated Technology for Verification and Analysis, Los Angeles, CA, USA.","DOI":"10.1007\/978-3-030-01090-4_30"},{"key":"ref_149","unstructured":"Torres, C.F., and Steichen, M. (2019, January 14\u201316). The art of the scam: Demystifying honeypots in ethereum smart contracts. Proceedings of the 28th USENIX Security Symposium (USENIX Security 19), Santa Clara, CA, USA."},{"key":"ref_150","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1145\/3416262","article-title":"MadMax: Analyzing the out-of-gas world of smart contracts","volume":"63","author":"Grech","year":"2020","journal-title":"Commun. ACM"},{"key":"ref_151","unstructured":"Mueller, B. (2018, January 9\u201313). Smashing Smart Contracts. Proceedings of the 9th HITB Security Conference, Amsterdam, The Netherlands. Available online: https:\/\/github.com\/muellerberndt\/smashing-smart-contracts\/blob\/master\/smashing-smart-contracts-1of1.pdf."},{"key":"ref_152","unstructured":"Ventuzelo, P. (2024, February 26). Octopus: Ethereum Smart Contract Security Analysis Tool. Available online: https:\/\/github.com\/FuzzingLabs\/octopus."},{"key":"ref_153","doi-asserted-by":"crossref","unstructured":"Torres, C.F., Sch\u00fctte, J., and State, R. (2018, January 3\u20137). Osiris: Hunting for integer bugs in ethereum smart contracts. Proceedings of the 34th Annual Computer Security Applications Conference, San Juan, PR, USA.","DOI":"10.1145\/3274694.3274737"},{"key":"ref_154","unstructured":"Suiche, M. (2024, February 08). Porosity: Decompiler and Security Analysis Tool for Ethereum Smart Contracts. Available online: https:\/\/github.com\/msuiche\/porosity."},{"key":"ref_155","unstructured":"PNF Software (2025, May 31). JEB Ethereum Plugin Documentation. Available online: https:\/\/www.pnfsoftware.com\/jeb\/manual\/ethereum\/."},{"key":"ref_156","doi-asserted-by":"crossref","unstructured":"Chinen, Y., Yanai, N., Cruz, J.P., and Okamura, S. (2020, January 2\u20136). RA: Hunting for re-entrancy attacks in ethereum smart contracts via static analysis. Proceedings of the 2020 IEEE International Conference on Blockchain (Blockchain), Virtual.","DOI":"10.1109\/Blockchain50366.2020.00048"},{"key":"ref_157","unstructured":"Krupp, J., and Rossow, C. (2018, January 15\u201317). teEther: Gnawing at ethereum to automatically exploit smart contracts. Proceedings of the 27th USENIX Security Symposium (USENIX Security 18), Baltimore, MD, USA."},{"key":"ref_158","unstructured":"Brent, L., Jurisevic, A., Kong, M., Liu, E., Gauthier, F., Gramoli, V., Holz, R., and Scholz, B. (2018). Vandal: A scalable security analysis framework for smart contracts. arXiv."},{"key":"ref_159","doi-asserted-by":"crossref","unstructured":"Colombo, C., and Leucker, M. (2018, January 10\u201313). Monitoring Smart Contracts: ContractLarva and Open Challenges Beyond. Proceedings of the Runtime Verification, Limassol, Cyprus.","DOI":"10.1007\/978-3-030-03769-7"},{"key":"ref_160","unstructured":"Stegeman, L. (2018). Solitor: Runtime Verification of Smart Contracts on the Ethereum Network. [Master\u2019s Thesis, University of Twente]. Available online: http:\/\/essay.utwente.nl\/76902\/."},{"key":"ref_161","doi-asserted-by":"crossref","unstructured":"Wang, H., Li, Y., Lin, S.W., Ma, L., and Liu, Y. (2019, January 25\u201331). Vultron: Catching vulnerable smart contracts once and for all. Proceedings of the 2019 IEEE\/ACM 41st International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER), Montreal, QC, Canada.","DOI":"10.1109\/ICSE-NIER.2019.00009"},{"key":"ref_162","doi-asserted-by":"crossref","unstructured":"Jiang, B., Liu, Y., and Chan, W.K. (2018, January 3\u20137). Contractfuzzer: Fuzzing smart contracts for vulnerability detection. Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, Montpellier, France.","DOI":"10.1145\/3238147.3238177"},{"key":"ref_163","unstructured":"Nguyen, T.D., Pham, L.H., Sun, J., Lin, Y., and Minh, Q.T. (July, January 27). sfuzz: An efficient adaptive fuzzer for solidity smart contracts. Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering, Seoul, Republic of Korea."},{"key":"ref_164","doi-asserted-by":"crossref","unstructured":"Chen, T., Cao, R., Li, T., Luo, X., Gu, G., Zhang, Y., Liao, Z., Zhu, H., Chen, G., and He, Z. (2020, January 23\u201326). SODA: A Generic Online Detection Framework for Smart Contracts. Proceedings of the NDSS, San Diego, CA, USA.","DOI":"10.14722\/ndss.2020.24449"},{"key":"ref_165","doi-asserted-by":"crossref","unstructured":"Gao, J., Liu, H., Liu, C., Li, Q., Guan, Z., and Chen, Z. (2019, January 25\u201331). Easyflow: Keep ethereum away from overflow. Proceedings of the 2019 IEEE\/ACM 41st International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), Montreal, QC, Canada.","DOI":"10.1109\/ICSE-Companion.2019.00029"},{"key":"ref_166","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3158136","article-title":"Online detection of effectively callback free objects with applications to smart contracts","volume":"2","author":"Grossman","year":"2017","journal-title":"Proc. ACM Program. Lang."},{"key":"ref_167","unstructured":"Pace, G. (2024, February 08). ContractLarva: A Tool for Runtime Monitoring of Ethereum Smart Contracts. Available online: https:\/\/github.com\/gordonpace\/contractLarva."},{"key":"ref_168","unstructured":"NTU SRSLab (2024, February 26). ModCon: Ethereum Smart Contract Modification Detection Tool. Available online: https:\/\/github.com\/ntu-SRSLab\/ModCon."},{"key":"ref_169","unstructured":"Stegeman, L. (2024, February 26). Solitor: Ethereum Smart Contract Runtime Monitoring Tool. Available online: https:\/\/github.com\/LarsStegeman\/EthereumRuntimeMonitoring."},{"key":"ref_170","unstructured":"NTU SRSLab (2024, February 26). Vultron: Ethereum Smart Contract Vulnerability Detection Tool. Available online: https:\/\/github.com\/ntu-SRSLab\/vultron."},{"key":"ref_171","unstructured":"Bell, G. (2024, February 13). ContractFuzzer: Fuzz Testing Tool for Ethereum Smart Contracts. Available online: https:\/\/github.com\/gongbell\/ContractFuzzer."},{"key":"ref_172","unstructured":"Tai, D. (2024, February 27). sFuzz: Ethereum Smart Contract Fuzz Testing Tool. Available online: https:\/\/github.com\/duytai\/sFuzz."},{"key":"ref_173","unstructured":"PandAbox Development (2024, February 27). SODA: Solidity Contract Data Analyzer. Available online: https:\/\/github.com\/pandabox-dev\/SODA."},{"key":"ref_174","unstructured":"Gao, J. (2024, February 27). EasyFlow: Ethereum Smart Contract Static Analysis Tool. Available online: https:\/\/github.com\/Jianbo-Gao\/EasyFlow."},{"key":"ref_175","unstructured":"Grinberg, S. (2024, February 21). ECFChecker. Available online: https:\/\/github.com\/shellygr\/ECFChecker."},{"key":"ref_176","doi-asserted-by":"crossref","unstructured":"Akca, S., Rajan, A., and Peng, C. (2019, January 2\u20135). SolAnalyser: A Framework for Analysing and Testing Smart Contracts. Proceedings of the 2019 26th Asia-Pacific Software Engineering Conference (APSEC), Putrajaya, Malaysia.","DOI":"10.1109\/APSEC48747.2019.00071"},{"key":"ref_177","doi-asserted-by":"crossref","unstructured":"Mossberg, M., Manzano, F., Hennenfent, E., Groce, A., Grieco, G., Feist, J., Brunson, T., and Dinaburg, A. (2019, January 10\u201315). Manticore: A user-friendly symbolic execution framework for binaries and smart contracts. Proceedings of the 2019 34th IEEE\/ACM International Conference on Automated Software Engineering (ASE), San Diego, CA, USA.","DOI":"10.1109\/ASE.2019.00133"},{"key":"ref_178","doi-asserted-by":"crossref","unstructured":"di Angelo, M., Durieux, T., Ferreira, J.F., and Salzer, G. (2023, January 11\u201315). SmartBugs 2.0: An Execution Framework for Weakness Detection in Ethereum Smart Contracts. Proceedings of the 38th IEEE\/ACM International Conference on Automated Software Engineering (ASE), Luxembourg.","DOI":"10.1109\/ASE56229.2023.00060"},{"key":"ref_179","unstructured":"Akca, S. (2024, February 25). SolAnalyser: Solidity Smart Contract Security Analyzer. Available online: https:\/\/github.com\/sefaakca\/SolAnalyser."},{"key":"ref_180","unstructured":"Trail of Bits (2024, February 08). Manticore: Symbolic Execution Tool for Analysis of Smart Contracts and Binaries. Available online: https:\/\/github.com\/trailofbits\/manticore."},{"key":"ref_181","unstructured":"Nikoli\u0107, I. (2024, February 08). MAIAN: A Novel Mitigation for Reentrancy Attacks. Available online: https:\/\/github.com\/ivicanikolicsg\/MAIAN."},{"key":"ref_182","unstructured":"SmartBugs (2024, February 24). SmartBugs: Smart Contract Static Analysis. Available online: https:\/\/github.com\/smartbugs\/smartbugs."},{"key":"ref_183","unstructured":"Pierro, A. (2024, March 22). SPASO (PArser for SOlidity). Available online: https:\/\/github.com\/aphd\/paso."},{"key":"ref_184","unstructured":"Pierro, G.A., and Tonelli, R. (2020, January 18). PASO: A Web-Based Parser for Solidity Language Analysis. Proceedings of the 2020 IEEE International Workshop on Blockchain Oriented Software Engineering (IWBOSE), London, ON, Canada."},{"key":"ref_185","doi-asserted-by":"crossref","first-page":"2874","DOI":"10.1109\/TSE.2020.2971482","article-title":"Checking smart contracts with structural code embedding","volume":"47","author":"Gao","year":"2020","journal-title":"IEEE Trans. Softw. Eng."},{"key":"ref_186","doi-asserted-by":"crossref","unstructured":"Camino, R., Torres, C.F., Baden, M., and State, R. (2019). A Data Science Approach for Honeypot Detection in Ethereum. arXiv.","DOI":"10.1109\/ICBC48266.2020.9169396"},{"key":"ref_187","unstructured":"Zhuang, Y., Liu, Z., Qian, P., Liu, Q., Wang, X., and He, Q. (2021, January 7\u201315). Smart Contract Vulnerability Detection using Graph Neural Network. Proceedings of the IJCAI, Yokohama, Japan."},{"key":"ref_188","unstructured":"Qian, P. (2024, February 21). GNNSCVulDetector: Graph Neural Network-Based Smart Contract Vulnerability Detector. Available online: https:\/\/github.com\/Messi-Q\/GNNSCVulDetector."},{"key":"ref_189","doi-asserted-by":"crossref","unstructured":"Liu, Z., Qian, P., Wang, X., Zhu, L., He, Q., and Ji, S. (2021). Smart contract vulnerability detection: From pure neural network to interpretable graph feature and expert pattern fusion. arXiv.","DOI":"10.24963\/ijcai.2021\/379"},{"key":"ref_190","doi-asserted-by":"crossref","first-page":"19685","DOI":"10.1109\/ACCESS.2020.2969429","article-title":"Towards automated reentrancy detection for smart contracts based on sequential models","volume":"8","author":"Qian","year":"2020","journal-title":"IEEE Access"},{"key":"ref_191","doi-asserted-by":"crossref","unstructured":"Yu, X., Zhao, H., Hou, B., Ying, Z., and Wu, B. (July, January 30). Deescvhunter: A deep learning-based framework for smart contract vulnerability detection. Proceedings of the 2021 International Joint Conference on Neural Networks (IJCNN), Rome, Italy.","DOI":"10.1109\/IJCNN52387.2021.9534324"},{"key":"ref_192","doi-asserted-by":"crossref","unstructured":"Ashizawa, N., Yanai, N., Cruz, J.P., and Okamura, S. (2022, January 10\u201314). Eth2Vec: Learning contract-wide code representations for vulnerability detection on Ethereum smart contracts. Proceedings of the 3rd ACM International Symposium on Blockchain and Secure Critical Infrastructure, Melbourne, Australia.","DOI":"10.1016\/j.bcra.2022.100101"},{"key":"ref_193","doi-asserted-by":"crossref","unstructured":"Nguyen, H.H., Nguyen, N.M., Xie, C., Ahmadi, Z., Kudendo, D., Doan, T.N., and Jiang, L. (2022, January 13\u201316). MANDO: Multi-level heterogeneous graph embeddings for fine-grained detection of smart contract vulnerabilities. Proceedings of the 2022 IEEE 9th International Conference on Data Science and Advanced Analytics (DSAA), Online.","DOI":"10.1109\/DSAA54385.2022.10032337"},{"key":"ref_194","first-page":"1296","article-title":"Combining graph neural networks with expert knowledge for smart contract vulnerability detection","volume":"35","author":"Liu","year":"2021","journal-title":"IEEE Trans. Knowl. Data Eng."},{"key":"ref_195","doi-asserted-by":"crossref","unstructured":"He, J., Balunovi\u0107, M., Ambroladze, N., Tsankov, P., and Vechev, M. (2019, January 11\u201315). Learning to Fuzz from Symbolic Execution with Application to Smart Contracts. Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, London, UK.","DOI":"10.1145\/3319535.3363230"},{"key":"ref_196","doi-asserted-by":"crossref","unstructured":"Su, J., Dai, H.N., Zhao, L., Zheng, Z., and Luo, X. (2023, January 10\u201314). Effectively Generating Vulnerable Transaction Sequences in Smart Contracts with Reinforcement Learning-guided Fuzzing. Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering, Rochester, MI, USA.","DOI":"10.1145\/3551349.3560429"},{"key":"ref_197","doi-asserted-by":"crossref","unstructured":"Zhang, Z., Lei, Y., Yan, M., Yu, Y., Chen, J., Wang, S., and Mao, X. (2022, January 10\u201314). Reentrancy vulnerability detection and localization: A deep learning based two-phase approach. Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering, Rochester, MI, USA.","DOI":"10.1145\/3551349.3560428"},{"key":"ref_198","unstructured":"Tann, W.J.W., Han, X.J., Gupta, S.S., and Ong, Y.S. (2018). Towards safer smart contracts: A sequence learning approach to detecting security threats. arXiv."},{"key":"ref_199","doi-asserted-by":"crossref","unstructured":"Liao, J.W., Tsai, T.T., He, C.K., and Tien, C.W. (2019, January 22\u201325). Soliaudit: Smart contract vulnerability assessment based on machine learning and fuzz testing. Proceedings of the 2019 Sixth International Conference on Internet of Things: Systems, Management and Security (IOTSMS), Granada, Spain.","DOI":"10.1109\/IOTSMS48152.2019.8939256"},{"key":"ref_200","doi-asserted-by":"crossref","first-page":"100171","DOI":"10.1016\/j.bcra.2023.100171","article-title":"Unveiling vulnerable smart contracts: Toward profiling vulnerable smart contracts using genetic algorithm and generating benchmark dataset","volume":"5","author":"HajiHosseinKhani","year":"2024","journal-title":"Blockchain Res. Appl."},{"key":"ref_201","doi-asserted-by":"crossref","unstructured":"Ren, M., Yin, Z., Ma, F., Xu, Z., Jiang, Y., Sun, C., Li, H., and Cai, Y. (2021, January 11\u201317). Empirical evaluation of smart contract testing: What is the best choice?. Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, Aarhus, Denmark.","DOI":"10.1145\/3460319.3464837"},{"key":"ref_202","unstructured":"Durieux, T., Ferreira, J.F., Abreu, R., and Cruz, P. (July, January 27). Empirical review of automated analysis tools on 47,587 ethereum smart contracts. Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering, Seoul, Republic of Korea."},{"key":"ref_203","doi-asserted-by":"crossref","unstructured":"Ghaleb, A., and Pattabiraman, K. (2020, January 18\u201322). How effective are smart contract analysis tools? Evaluating smart contract static analysis tools using bug injection. Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event.","DOI":"10.1145\/3395363.3397385"},{"key":"ref_204","doi-asserted-by":"crossref","unstructured":"Khan, D., Jung, L.T., and Hashmani, M.A. (2021). Systematic literature review of challenges in blockchain scalability. Appl. Sci., 11.","DOI":"10.3390\/app11209372"},{"key":"ref_205","doi-asserted-by":"crossref","first-page":"100596","DOI":"10.1016\/j.cosrev.2023.100596","article-title":"Graph-based deep learning techniques for remote sensing applications: Techniques, taxonomy, and applications\u2014A comprehensive review","volume":"50","author":"Khlifi","year":"2023","journal-title":"Comput. Sci. Rev."},{"key":"ref_206","doi-asserted-by":"crossref","unstructured":"Ammar, A., Koubaa, A., Benjdira, B., Nacar, O., and Sibaee, S. (2024). Prediction of Arabic Legal Rulings Using Large Language Models. Electronics, 13.","DOI":"10.3390\/electronics13040764"},{"key":"ref_207","doi-asserted-by":"crossref","first-page":"3043","DOI":"10.1007\/s10618-022-00867-8","article-title":"A comprehensive taxonomy for explainable artificial intelligence: A systematic survey of surveys on methods and concepts","volume":"38","author":"Schwalbe","year":"2024","journal-title":"Data Min. Knowl. Discov."},{"key":"ref_208","unstructured":"\u00c1lvarez, I.A., Gramlich, V., and Sedlmeir, J. (2024). Unsealing the secrets of blockchain consensus: A systematic comparison of the formal security of proof-of-work and proof-of-stake. arXiv."},{"key":"ref_209","doi-asserted-by":"crossref","unstructured":"Lv, P., Wang, Y., Wang, Y., and Zhou, Q. (2021, January 5\u20138). Potential risk detection system of hyperledger fabric smart contract based on static analysis. Proceedings of the 2021 IEEE Symposium on Computers and Communications (ISCC), Athens, Greece.","DOI":"10.1109\/ISCC53001.2021.9631249"},{"key":"ref_210","doi-asserted-by":"crossref","unstructured":"Lamela Seijas, P., Nemish, A., Smith, D., and Thompson, S. (2020, January 14). Marlowe: Implementing and analysing financial contracts on blockchain. Proceedings of the Financial Cryptography and Data Security: FC 2020 International Workshops, AsiaUSEC, CoDeFi, VOTING, and WTSC, Kota Kinabalu, Malaysia. Revised Selected Papers 24.","DOI":"10.1007\/978-3-030-54455-3_35"},{"key":"ref_211","unstructured":"Chakravarty, M., Kireev, R., MacKenzie, K., McHale, V., M\u00fcller, J., Nemish, A., Nester, C., Jones, M.P., Thompson, S., and Valentine, R. (2025, May 31). Functional Blockchain Contracts. Available online: https:\/\/americanblockchainpac.org\/wp-content\/uploads\/2022\/03\/Functional-Blockchain-Contracts.pdf."},{"key":"ref_212","unstructured":"Solana Foundation (2025, May 31). X-Ray: Open-Source Static Analyzer for Solana Smart Contracts. Available online: https:\/\/solanacompass.com\/learn\/breakpoint-24\/bp-2024-technical-talk-open-source-x-ray-solana-smart-contract-static-analysis."},{"key":"ref_213","unstructured":"Solana Documentation (2025, May 31). Radar\u2013Static Analysis Tool for Anchor Rust Programs. Available online: https:\/\/solana.com\/docs\/toolkit\/test-suite\/security-scanner."},{"key":"ref_214","unstructured":"Web3 Labs (2025, May 31). Ink! Verifier Service. Ensures Reproducible Bytecode Verification for Ink! Contracts. Available online: https:\/\/github.com\/web3labs\/ink-verifier-image."},{"key":"ref_215","unstructured":"Chainlink (2025, May 06). Cross-Chain Interoperability Protocol (CCIP). Available online: https:\/\/chain.link\/cross-chain."},{"key":"ref_216","unstructured":"Input Output Global (IOG) (2025, May 05). Marlowe. Available online: https:\/\/docs.cardano.org\/developer-resources\/smart-contracts\/marlowe."}],"container-title":["Computers"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-431X\/14\/6\/226\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:48:54Z","timestamp":1760032134000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-431X\/14\/6\/226"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,9]]},"references-count":216,"journal-issue":{"issue":"6","published-online":{"date-parts":[[2025,6]]}},"alternative-id":["computers14060226"],"URL":"https:\/\/doi.org\/10.3390\/computers14060226","relation":{},"ISSN":["2073-431X"],"issn-type":[{"type":"electronic","value":"2073-431X"}],"subject":[],"published":{"date-parts":[[2025,6,9]]}}}