{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,31]],"date-time":"2026-07-31T13:04:10Z","timestamp":1785503050219,"version":"3.56.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031945328","type":"print"},{"value":"9783031945335","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T00:00:00Z","timestamp":1748822400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T00:00:00Z","timestamp":1748822400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-031-94533-5_3","type":"book-chapter","created":{"date-parts":[[2025,8,31]],"date-time":"2025-08-31T19:32:34Z","timestamp":1756668754000},"page":"31-51","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Using Symbolic Model Execution to\u00a0Detect Vulnerabilities of\u00a0Smart Contracts"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/2.zoppoz.workers.dev:443\/https\/orcid.org\/0000-0002-9756-4675","authenticated-orcid":false,"given":"Chiara","family":"Braghin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/2.zoppoz.workers.dev:443\/https\/orcid.org\/0009-0005-7020-6607","authenticated-orcid":false,"given":"Giuseppe","family":"Del Castillo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/2.zoppoz.workers.dev:443\/https\/orcid.org\/0000-0002-1400-1026","authenticated-orcid":false,"given":"Elvinia","family":"Riccobene","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/2.zoppoz.workers.dev:443\/https\/orcid.org\/0009-0005-5956-3945","authenticated-orcid":false,"given":"Simone","family":"Valentini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,6,2]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","DOI":"10.1016\/j.pmcj.2020.101227","volume":"67","author":"M Almakhour","year":"2020","unstructured":"Almakhour, M., Sliman, L., Samhat, A.E., Mellouk, A.: Verification of smart contracts: a survey. Pervasive Mob. Comput. 67, 101227 (2020). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1016\/j.pmcj.2020.101227","journal-title":"Pervasive Mob. Comput."},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Alt, L., Blicha, M., Hyv\u00e4rinen, A.E., Sharygina, N.: SolCMC: solidity compiler\u2019s model checker. In: 34th International Conference on Computer Aided Verification, CAV 2022, pp. 325\u2013338. Springer, Cham (2022). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-031-13185-1_16","DOI":"10.1007\/978-3-031-13185-1_16"},{"key":"3_CR3","unstructured":"Andreessen Horowitz VC: Halmos (2025). https:\/\/2.zoppoz.workers.dev:443\/https\/github.com\/a16z\/halmos"},{"issue":"2","key":"3_CR4","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1002\/spe.1019","volume":"41","author":"P Arcaini","year":"2011","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E., Scandurra, P.: A model-driven process for engineering a toolset for a formal method. Softw. Pract. Experience 41(2), 155\u2013166 (2011). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1002\/spe.1019","journal-title":"Softw. Pract. Experience"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Bartoletti, M., Fioravanti, F., Matricardi, G., Pettinau, R., Sainas, F.: Towards benchmarking of solidity verification tools. In: 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), vol.\u00a0118, pp. 6:1\u20136:15. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.4230\/OASIcs.FMBC.2024.6","DOI":"10.4230\/OASIcs.FMBC.2024.6"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"Bombarda, A., Bonfanti, S., Gargantini, A., Riccobene, E., Scandurra, P.: ASMETA tool set for rigorous system design. In: Formal Methods, vol. 14934, pp. 492\u2013517. Springer, Cham (2025). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-031-71177-0_28","DOI":"10.1007\/978-3-031-71177-0_28"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"B\u00f6rger, E., Raschke, A.: Modeling Companion for Software Practitioners. Springer, Cham (2018). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-662-56641-1","DOI":"10.1007\/978-3-662-56641-1"},{"key":"3_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7","author":"E B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.: Abstract state machines: a method for high-level system design and analysis. Springer (2003). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-642-18216-7","journal-title":"Springer"},{"key":"3_CR9","doi-asserted-by":"publisher","unstructured":"Braghin, C., Cimato, S., Damiani, E., Baronchelli, M.: Designing smart-contract based auctions. In: Security with Intelligent Computing and Big-data Services, SICBS 2018, pp. 54\u201364. Springer, Cham (2020). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-030-16946-6_5","DOI":"10.1007\/978-3-030-16946-6_5"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Braghin, C., Riccobene, E., Valentini, S.: An ASM-based approach for security assessment of ethereum smart contracts. In: Proceedings of the 21st International Conference on Security and Cryptography, SECRYPT 2024, pp. 334\u2013344. SCITEPRESS (2024). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.5220\/0012858000003767","DOI":"10.5220\/0012858000003767"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Braghin, C., Riccobene, E., Valentini, S.: Modeling and verification of smart contracts with abstract state machines. In: Proceedings of the 39th ACM\/SIGAPP Symposium on Applied Computing, SAC 2024, pp. 1425\u20131432. Association for Computing Machinery, New York (2024). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/3605098.3636040","DOI":"10.1145\/3605098.3636040"},{"key":"3_CR12","unstructured":"Braghin, C., Riccobene, E., Valentini, S.: Ethereum Via ASM (2025). https:\/\/2.zoppoz.workers.dev:443\/https\/github.com\/smart-contract-verification\/ABZ2025"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"\u015etef\u0103nescu, A., Park, D., Yuwen, S., Li, Y., Ro\u015fu, G.: Semantics-based program verifiers for all languages. In: Proceedings of the 31th Confernce on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, pp. 74\u201391. ACM (2016). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/2983990.2984027","DOI":"10.1145\/2983990.2984027"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Del\u00a0Castillo, G.: Using symbolic execution to transform turbo abstract state machines into basic abstract state machines. In: 10th International Conference on Rigorous State-Based Methods, ABZ 2024. Lecture Notes in Computer Science, vol. 14759, pp. 215\u2013222. Springer, Cham (2024). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-031-63790-2_15","DOI":"10.1007\/978-3-031-63790-2_15"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Del\u00a0Castillo, G.: Using symbolic execution to transform turbo abstract state machines into basic abstract state machines (extended version) (2024). https:\/\/2.zoppoz.workers.dev:443\/https\/github.com\/constructum\/asm-symbolic-execution\/blob\/main\/doc\/2024--Del-Castillo--extended-version-of-ABZ-2024-paper.pdf","DOI":"10.1007\/978-3-031-63790-2_15"},{"key":"3_CR16","unstructured":"Del\u00a0Castillo, G.: ASM symbolic execution (2025). https:\/\/2.zoppoz.workers.dev:443\/https\/github.com\/constructum\/asm-symbolic-execution. version used for the experiments presented in this paper: https:\/\/2.zoppoz.workers.dev:443\/https\/github.com\/constructum\/asm-symbolic-execution\/tree\/32251c45d43b41f39cdbff061ddd64914976c244"},{"key":"3_CR17","unstructured":"Dfinity: Eliminating smart contract bugs with TLA+ (2023). https:\/\/2.zoppoz.workers.dev:443\/https\/medium.com\/dfinity\/eliminating-smart-contract-bugs-with-tla-e986aeb6da24"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Dxo, Soos, M., Paraskevopoulou, Z., Lundfall, M., Brockman, M.: Hevm, a fast symbolic execution framework for EVM bytecode. In: International Conference on Computer Aided Verification, pp. 453\u2013465. Springer, Cham (2024)","DOI":"10.1007\/978-3-031-65627-9_22"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Fekih, R.B., Lahami, M., Jmaiel, M., Bradai, S.: Formal verification of smart contracts based on model checking: an overview. In: IEEE International Confernce on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2023, pp.\u00a01\u20136 (2023). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1109\/WETICE57085.2023.10477834","DOI":"10.1109\/WETICE57085.2023.10477834"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Grieco, G., Song, W., Cygan, A., Feist, J., Groce, A.: Echidna: effective, usable, and fast fuzzing for smart contracts. In: Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, pp. 557\u2013560 (2020). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/3395363.3404366","DOI":"10.1145\/3395363.3404366"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Hildenbrandt, E., et\u00a0al.: KEVM: a complete formal semantics of the ethereum virtual machine. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pp. 204\u2013217. IEEE (2018)","DOI":"10.1109\/CSF.2018.00022"},{"key":"3_CR22","unstructured":"Jackson, D., Nandi, C., Sagiv, M.: Certora technology white paper. https:\/\/2.zoppoz.workers.dev:443\/https\/docs.certora.com\/en\/latest\/docs\/whitepaper\/index.html"},{"issue":"3","key":"3_CR23","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(3), 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"3_CR24","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-031-77382-2_10","volume-title":"Software Engineering and Formal Methods","author":"D Marmsoler","year":"2025","unstructured":"Marmsoler, D., Ahmed, A., Brucker, A.D.: Secure smart contracts with isabelle\/solidity. In: Madeira, A., Knapp, A. (eds.) Software Engineering and Formal Methods, pp. 162\u2013181. Springer, Cham (2025)"},{"key":"3_CR25","unstructured":"New Alchemy: A short history of Smart Contract hacks on Ethereum: A.k.a. why you need a smart contract security audit (2018). https:\/\/2.zoppoz.workers.dev:443\/https\/medium.com\/new-alchemy\/a-short-history-of-smart-contract-hacks-on-ethereum-1a30020b5fd"},{"key":"3_CR26","unstructured":"Runtime Verification Inc.: Kontrol (2025). https:\/\/2.zoppoz.workers.dev:443\/https\/github.com\/runtimeverification\/kontrol"},{"key":"3_CR27","unstructured":"Siegel, D.: Understanding The DAO Attack (2016). https:\/\/2.zoppoz.workers.dev:443\/https\/www.coindesk.com\/learn\/understanding-the-dao-attack\/"},{"key":"3_CR28","unstructured":"Sotnichek, M.: Formal verification of smart contracts with the K framework (2019). https:\/\/2.zoppoz.workers.dev:443\/https\/www.apriorit.com\/dev-blog\/592-formal-verification-with-k-framework"},{"key":"3_CR29","doi-asserted-by":"publisher","unstructured":"Tolmach, P., Li, Y., Lin, S.W., Liu, Y., Li, Z.: A survey of smart contract formal specification and verification. ACM Comput. Surv. 54(7) (2021). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1145\/3464421","DOI":"10.1145\/3464421"},{"key":"3_CR30","doi-asserted-by":"publisher","unstructured":"Valentini, S., Braghin, C., Riccobene, E.: A modeling and verification framework for ethereum smart contracts. In: 10th International Confernce on Rigorous State-Based Methods, ABZ 2024. Lecture Notes in Computer Science, vol. 14759, pp. 201\u2013207. Springer, Cham (2024). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-031-63790-2_13","DOI":"10.1007\/978-3-031-63790-2_13"},{"issue":"2014","key":"3_CR31","first-page":"1","volume":"151","author":"G Wood","year":"2014","unstructured":"Wood, G., et al.: Ethereum: a secure decentralised generalised transaction ledger. Ethereum Proj. Yellow Paper 151(2014), 1\u201332 (2014)","journal-title":"Ethereum Proj. Yellow Paper"},{"key":"3_CR32","doi-asserted-by":"publisher","unstructured":"Zhang, Z., Zhang, B., Xu, W., Lin, Z.: Demystifying exploitable bugs in smart contracts. In: 2023 IEEE\/ACM 45th International Conference on Software Engineering, ICSE, pp. 615\u2013627. IEEE (2023). https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1109\/ICSE48619.2023.00061","DOI":"10.1109\/ICSE48619.2023.00061"}],"container-title":["Lecture Notes in Computer Science","Rigorous State-Based Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-94533-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,31]],"date-time":"2026-07-31T12:17:19Z","timestamp":1785500239000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/link.springer.com\/10.1007\/978-3-031-94533-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,2]]},"ISBN":["9783031945328","9783031945335"],"references-count":32,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1007\/978-3-031-94533-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,2]]},"assertion":[{"value":"2 June 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ABZ","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Rigorous State-Based Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"D\u00fcsseldorf","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"abz2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2.zoppoz.workers.dev:443\/https\/abz-conf.org\/site\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}