{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,7]],"date-time":"2026-06-07T04:48:51Z","timestamp":1780807731523,"version":"3.54.1"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2025,3,3]],"date-time":"2025-03-03T00:00:00Z","timestamp":1740960000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"crossref","award":["EP\/X027619\/1"],"award-info":[{"award-number":["EP\/X027619\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,6,30]]},"abstract":"<jats:p>Smart contracts are computer programs designed to automate legal agreements. They are usually developed in a high-level programming language, the most popular of which is Solidity. Every day, hundreds of thousands of new contracts are deployed managing millions of dollars\u2019 worth of transactions. As for every computer program, smart contracts may contain bugs which can be exploited. However, since smart contracts are often used to automate financial transactions, such exploits may result in huge economic losses. In general, it is estimated that since 2019, more than $5B was stolen due to vulnerabilities in smart contracts.<\/jats:p>\n          <jats:p>This article addresses the issue of smart contract vulnerabilities by introducing an executable denotational semantics for Solidity within the Isabelle\/HOL interactive theorem prover. This formal semantics serves as the basis for an interactive program verification environment for Solidity smart contracts. To evaluate our semantics, we integrate grammar-based fuzzing with symbolic execution to automatically test it against the Solidity reference implementation. The article concludes by showcasing the formal verification of Solidity programs, exemplified through the verification of a basic Solidity token.<\/jats:p>","DOI":"10.1145\/3700601","type":"journal-article","created":{"date-parts":[[2024,10,15]],"date-time":"2024-10-15T11:12:34Z","timestamp":1728990754000},"page":"1-56","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Isabelle\/Solidity: A deep embedding of Solidity in Isabelle\/HOL"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2859-7673","authenticated-orcid":false,"given":"Diego","family":"Marmsoler","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Exeter, Exeter, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6355-1200","authenticated-orcid":false,"given":"Achim D.","family":"Brucker","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Exeter, Exeter, United Kingdom of Great Britain and Northern Ireland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,3,3]]},"reference":[{"key":"e_1_3_4_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6"},{"key":"e_1_3_4_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61467-6_2"},{"key":"e_1_3_4_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.pmcj.2020.101227"},{"key":"e_1_3_4_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57826-9_127"},{"key":"e_1_3_4_6_2","unstructured":"Solidity Authors. 2021. Solidity Documentation. Retrieved May 1 2021 from https:\/\/docs.soliditylang.org\/en\/v0.5.16\/"},{"key":"e_1_3_4_7_2","unstructured":"Solidity Authors. 2024. Solidity Developer Survey 2023 Results. Retrieved 28 October 2024 from https:\/\/soliditylang.org\/blog\/2024\/04\/03\/solidity-developer-survey-2023-results\/"},{"key":"e_1_3_4_8_2","unstructured":"T. Bahrynovska. 2017. History of Ethereum Security Vulnerabilities Hacks and Their Fixes. Retrieved 28 October 2024 from https:\/\/web.archive.org\/web\/20190628084427\/https:\/\/applicature.com\/blog\/blockchain-technology\/history-of-ethereum-security-vulnerabilities-hacks-and-their-fixes"},{"key":"e_1_3_4_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31500-9_15"},{"key":"e_1_3_4_10_2","first-page":"19","volume-title":"TPHOLs","author":"Berghofer Stefan","year":"1999","unstructured":"Stefan Berghofer and Markus Wenzel. 1999. Inductive datatypes in HOL \u2014 lessons learned in formal-logic engineering. In TPHOLs, Yves Bertot, Gilles Dowek, Laurent Th\u00e9ry, Andr\u00e9 Hirschowitz, and Christine Paulin (Eds.). Springer, 19\u201336."},{"key":"e_1_3_4_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38348-9_19"},{"key":"e_1_3_4_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993611"},{"key":"e_1_3_4_13_2","series-title":"IFIP Transactions","first-page":"129","volume-title":"Proceedings of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience","volume":"10","author":"Boulton Richard","year":"1993","unstructured":"Richard Boulton, Andrew Gordon, Michael J. C. Gordon, John Harrison, John Herbert, and John Van Tassel. 1993. Experience with embedding hardware description languages in HOL. In Proceedings of the International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, Victoria Stavridou, Thomas F. Melham, and Raymond T. Boute (Eds.). IFIP Transactions, Vol. A-10, 129\u2013156."},{"key":"e_1_3_4_14_2","article-title":"AutoCorres2","author":"Brecknell Matthew","year":"2024","unstructured":"Matthew Brecknell, David Greenaway, Johannes H\u00f6lzl, Fabian Immler, Gerwin Klein, Rafal Kolanski, Japheth Lim, Michael Norrish, Norbert Schirmer, Salomon Sickert, Thomas Sewell, Harvey Tuch, and Simon Wimmer. 2024. AutoCorres2. Archive of Formal Proofs (2024). Retrieved from https:\/\/isa-afp.org\/entries\/AutoCorres2.html","journal-title":"Archive of Formal Proofs"},{"key":"e_1_3_4_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_14"},{"key":"e_1_3_4_16_2","unstructured":"Gertrude Chavez-Dreyfuss. 2016. Sweden Tests Blockchain Technology for Land Registry. Retrieved 28 October 2024 from https:\/\/web.archive.org\/web\/20230506142211\/https:\/\/www.reuters.com\/article\/us-sweden-blockchain\/sweden-tests-blockchain-technology-for-landregistry-idUSKCN0Z22KV\/"},{"key":"e_1_3_4_17_2","volume-title":"Cryptocurrency Crime and Anti-Money Laundering Report","year":"2021","unstructured":"CipherTrace. 2021. Cryptocurrency Crime and Anti-Money Laundering Report. Technical Report. Retrieved from https:\/\/ciphertrace.com\/cryptocurrency-crime-and-anti-money-laundering-report-august-2021\/"},{"key":"e_1_3_4_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_16"},{"key":"e_1_3_4_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-43725-1_11"},{"key":"e_1_3_4_20_2","first-page":"1","volume-title":"VALID","author":"Crosara Marco","year":"2019","unstructured":"Marco Crosara, Gabriele Centurino, and Vincenzo Arceri. 2019. Towards an operational semantics for solidity. In VALID, Jos van Rooyen, Samuele Buro, Marco Campion, and Michele Pasqua (Eds.). IARIA, 1\u20136."},{"key":"e_1_3_4_21_2","volume-title":"Proceedings of the SEFM","year":"2021","unstructured":"DM and A. D. Brucker. 2021. A denotational semantics of solidity in Isabelle\/HOL. In Proceedings of the SEFM."},{"key":"e_1_3_4_22_2","volume-title":"Proceedings of the OBD","year":"2016","unstructured":"Asaph Azaria, Ariel Ekblaw, Thiago Vieira, and Andrew Lippman. 2016. Medrec: Using blockchain for medical data access and permission management. In Proceedings of the OBD."},{"key":"e_1_3_4_23_2","unstructured":"Gaurav Batra R\u00e9my Olson Shilpi Pathak Nick Santhanam and Harish Soundararajan. 2019. Blockchain 2.0: What\u2019s in Store for the Two Ends? Retrieved 28 October 2024 from https:\/\/web.archive.org\/web\/20240708010430\/https:\/\/www.mckinsey.com\/industries\/industrials-and-electronics\/our-insights\/blockchain-2-0-whats-in-store-for-the-two-ends-semiconductors-suppliers-and-industrials-consumers"},{"key":"e_1_3_4_24_2","doi-asserted-by":"publisher","unstructured":"Jan Mendling Ingo Weber Wil Van Der Aalst Jan Vom Brocke Cristina Cabanillas Florian Daniel S\u00f8ren Debois Claudio Di Ciccio Marlon Dumas Schahram Dustdar Avigdor Gal Luciano Garc\u00eda-Ba\u00f1uelos Guido Governatori Richard Hull Marcello La Rosa Henrik Leopold Frank Leymann Jan Recker Manfred Reichert Hajo A. Reijers Stefanie Rinderle-Ma Andreas Solti Michael Rosemann Stefan Schulte Munindar P. Singh Tijs Slaats Mark Staples Barbara Weber Matthias Weidlich Mathias Weske Xiwei Xu and Liming Zhu. 2018. Blockchains for business process management - challenges and opportunities. ACM Trans. Manage. Inf. Syst. 9 1 (February 2018). DOI:10.1145\/3183367","DOI":"10.1145\/3183367"},{"key":"e_1_3_4_25_2","unstructured":"Gartner. 2019. Forecast: Blockchain Business Value Worldwide 2017-2030. Retrieved 28 October 2024 from https:\/\/web.archive.org\/web\/20240123074027\/https:\/\/www.gartner.com\/en\/documents\/3627117"},{"key":"e_1_3_4_26_2","unstructured":"D. Goodin. 2021. Really Stupid \u201cSmart Contract\u201d Bug Let Hackers Steal $31 Million in Digital Coin. Retrieved 28 October 2024 from https:\/\/arstechnica.com\/information-technology\/2021\/12\/hackers-drain-31-million-from-cryptocurrency-service-monox-finance\/"},{"key":"e_1_3_4_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_8"},{"key":"e_1_3_4_28_2","unstructured":"Florian Haftmann and Lukas Bulwahn. 2023. Code Generation from Isabelle\/HOL Theories. Retrieved 28 October 2024 from http:\/\/isabelle.in.tum.de\/doc\/codegen.pdf"},{"key":"e_1_3_4_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-41600-3_11"},{"key":"e_1_3_4_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_9"},{"key":"e_1_3_4_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00066"},{"key":"e_1_3_4_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45234-6_4"},{"key":"e_1_3_4_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_11"},{"key":"e_1_3_4_34_2","unstructured":"J. Kelly. 2016. Banks Adopting Blockchain \u2018Dramatically Faster\u2019 than Expected: IBM. Retrieved 28 October 2024 from https:\/\/www.reuters.com\/article\/technology\/banks-adopting-blockchain-dramatically-faster-than-expected-ibm-idUSKCN11Y28G\/"},{"key":"e_1_3_4_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_4_36_2","article-title":"IMP2\u2014simple program verification in Isabelle\/HOL","author":"Lammich Peter","year":"2019","unstructured":"Peter Lammich and Simon Wimmer. 2019. IMP2\u2014simple program verification in Isabelle\/HOL. Archive of Formal Proofs (2019). Retrieved from https:\/\/isa-afp.org\/entries\/IMP2.html. Formal proof development.","journal-title":"Archive of Formal Proofs"},{"key":"e_1_3_4_37_2","unstructured":"Defi Llama. 2024. TVL Breakdown by Smart Contract Language. Retrieved 3 June 2024 from https:\/\/defillama.com\/languages"},{"key":"e_1_3_4_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-92124-8_23"},{"key":"e_1_3_4_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-09827-7_7"},{"key":"e_1_3_4_40_2","article-title":"Isabelle\/Solidity: A deep embedding of solidity in Isabelle\/HOL","author":"Marmsoler Diego","year":"2022","unstructured":"Diego Marmsoler and Achim D. Brucker. 2022. Isabelle\/Solidity: A deep embedding of solidity in Isabelle\/HOL. Archive of Formal Proofs (2022). Retrieved from https:\/\/isa-afp.org\/entries\/Solidity.html","journal-title":"Archive of Formal Proofs"},{"key":"e_1_3_4_41_2","first-page":"270","volume-title":"Principles of Security and Trust","author":"Mavridou Anastasia","year":"2018","unstructured":"Anastasia Mavridou and Aron Laszka. 2018. Tool demonstration: FSolidM for designing secure ethereum smart contracts. In Principles of Security and Trust, Lujo Bauer and Ralf K\u00fcsters (Eds.). Springer, 270\u2013277."},{"key":"e_1_3_4_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32101-7_27"},{"key":"e_1_3_4_43_2","unstructured":"S. Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system. (2008). Retrieved 28 October 2024 from https:\/\/bitcoin.org\/bitcoin.pdf"},{"key":"e_1_3_4_44_2","unstructured":"BBC News. 2021. Hackers Steal $600m in Major Cryptocurrency Heist. Retrieved 28 October 2024 from https:\/\/www.cnbc.com\/2021\/08\/23\/poly-network-hacker-returns-remaining-cryptocurrency.html"},{"key":"e_1_3_4_45_2","doi-asserted-by":"publisher","unstructured":"Tobias Nipkow. 1998. Winskel is (almost) right: Towards a mechanized semantics textbook. 10 2 (1998) 171\u2013186. DOI:10.1007\/s001650050009","DOI":"10.1007\/s001650050009"},{"key":"e_1_3_4_46_2","series-title":"LNCS","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic","author":"Nipkow Tobias","year":"2002","unstructured":"Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2002. Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. LNCS, Vol. 2283. Springer."},{"key":"e_1_3_4_47_2","volume-title":"Proceedings of the USENIX Security","author":"Perez Daniel","year":"2021","unstructured":"Daniel Perez and Ben Livshits. 2021. Smart contract vulnerabilities: Vulnerable does not imply exploited. In Proceedings of the USENIX Security. USENIX Association."},{"key":"e_1_3_4_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-62077-6_7"},{"key":"e_1_3_4_49_2","volume-title":"Verification of Sequential Imperative Programs in Isabelle\/HOL","author":"Schirmer Norbert","year":"2006","unstructured":"Norbert Schirmer. 2006. Verification of Sequential Imperative Programs in Isabelle\/HOL. Ph. D. Dissertation. Technische Universit\u00e4t M\u00fcnchen."},{"key":"e_1_3_4_50_2","article-title":"A sequential imperative programming language syntax, semantics, hoare logics and verification environment","author":"Schirmer Norbert","year":"2008","unstructured":"Norbert Schirmer. 2008. A sequential imperative programming language syntax, semantics, hoare logics and verification environment. Archive of Formal Proofs (2008). Retrieved from http:\/\/afp.sf.net\/entries\/Simpl.shtml, Formal proof development.","journal-title":"Archive of Formal Proofs"},{"key":"e_1_3_4_51_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-323-96146-2.00028-0"},{"key":"e_1_3_4_52_2","article-title":"Certification monads","author":"Sternagel Christian","year":"2014","unstructured":"Christian Sternagel and Ren\u00e9 Thiemann. 2014. Certification monads. Archive of Formal Proofs (2014). https:\/\/www.isa-afp.org\/entries\/Certification_Monads.shtml. Formal proof development.","journal-title":"Archive of Formal Proofs"},{"key":"e_1_3_4_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3464421"},{"key":"e_1_3_4_54_2","article-title":"Clean\u2014an abstract imperative programming language and its theory","author":"Tuong Fr\u00e9deric","year":"2019","unstructured":"Fr\u00e9deric Tuong and Burkhart Wolff. 2019. Clean\u2014an abstract imperative programming language and its theory. Archive of Formal Proofs (2019). Retrieved from https:\/\/isa-afp.org\/entries\/Clean.html, Formal proof development.","journal-title":"Archive of Formal Proofs"},{"key":"e_1_3_4_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02880-3_8"},{"key":"e_1_3_4_56_2","volume-title":"Ethereum: A Secure Decentralised Generalised Transation Ledger (Version 2021-04-21)","author":"Wood Gavin","year":"2021","unstructured":"Gavin Wood. 2021. Ethereum: A Secure Decentralised Generalised Transation Ledger (Version 2021-04-21). Technical Report. Ethereum."},{"key":"e_1_3_4_57_2","unstructured":"YCharts.com. 2022. Ethereum Transactions Per Day. Retrieved 28 October 2024 from https:\/\/ycharts.com\/indicators\/ethereum_transactions_per_day#:~:text=Ethereum%20Transactions%20Per%20Day%20is 6.17%25%20from%20one%20year%20ago"},{"key":"e_1_3_4_58_2","unstructured":"B. Yurcan. 2016. How Blockchain Fits into the Future of Digital Identity. Retrieved 28 October 2024 from https:\/\/web.archive.org\/web\/20240527151902\/https:\/\/www.americanbanker.com\/news\/how-blockchain-fits-into-the-future-of-digital-identity"},{"key":"e_1_3_4_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03592-1_13"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3700601","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3700601","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:17:28Z","timestamp":1750295848000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3700601"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,3]]},"references-count":58,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6,30]]}},"alternative-id":["10.1145\/3700601"],"URL":"https:\/\/doi.org\/10.1145\/3700601","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,3,3]]},"assertion":[{"value":"2023-12-18","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-09-24","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-03","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}