{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T17:48:20Z","timestamp":1772041700773,"version":"3.50.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031274800","type":"print"},{"value":"9783031274817","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"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":[[2023]]},"DOI":"10.1007\/978-3-031-27481-7_32","type":"book-chapter","created":{"date-parts":[[2023,3,2]],"date-time":"2023-03-02T14:03:10Z","timestamp":1677765790000},"page":"571-583","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Formal and\u00a0Executable Semantics of\u00a0the\u00a0Ethereum Virtual Machine in\u00a0Dafny"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4317-5025","authenticated-orcid":false,"given":"Franck","family":"Cassez","sequence":"first","affiliation":[]},{"given":"Joanne","family":"Fuller","sequence":"additional","affiliation":[]},{"given":"Milad K.","family":"Ghale","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4535-9677","authenticated-orcid":false,"given":"David J.","family":"Pearce","sequence":"additional","affiliation":[]},{"given":"Horacio M. A.","family":"Quiles","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,3,3]]},"reference":[{"key":"32_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/978-3-030-01090-4_30","volume-title":"Automated Technology for Verification and Analysis","author":"E Albert","year":"2018","unstructured":"Albert, E., Gordillo, P., Livshits, B., Rubio, A., Sergey, I.: EthIR: a framework for high-level analysis of Ethereum bytecode. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 513\u2013520. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_30"},{"key":"32_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-030-35092-5_5","volume-title":"Verification and Evaluation of Computer and Communication Systems","author":"E Albert","year":"2019","unstructured":"Albert, E., Gordillo, P., Rubio, A., Sergey, I.: Running on fumes. In: Ganty, P., Ka\u00e2niche, M. (eds.) VECoS 2019. LNCS, vol. 11847, pp. 63\u201378. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-35092-5_5"},{"key":"32_CR3","doi-asserted-by":"publisher","unstructured":"Amani, S., B\u00e9gel, M., Bortin, M., Staples, M.: Towards verifying Ethereum smart contract bytecode in Isabelle\/HOL. In: Andronick, J., Felty, A.P. (eds.) Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, 8\u20139 January 2018, pp. 66\u201377. ACM (2018). https:\/\/doi.org\/10.1145\/3167084","DOI":"10.1145\/3167084"},{"key":"32_CR4","doi-asserted-by":"publisher","unstructured":"Badruddoja, S., Dantu, R., He, Y., Upadhayay, K., Thompson, M.: Making smart contracts smarter. In: 2021 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), pp. 1\u20133 (2021). https:\/\/doi.org\/10.1109\/ICBC51069.2021.9461148","DOI":"10.1109\/ICBC51069.2021.9461148"},{"key":"32_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74113-8","volume-title":"The Calculus of Computation - Decision Procedures with Applications to Verification","author":"AR Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation - Decision Procedures with Applications to Verification. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74113-8"},{"key":"32_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-031-15008-1_5","volume-title":"Formal Methods for Industrial Critical Systems","author":"F Cassez","year":"2022","unstructured":"Cassez, F., Fuller, J., Anton Quiles, H.M.: Deductive verification of smart contracts with Dafny. In: Groote, J.F., Huisman, M. (eds.) FMICS 2022. LNCS, vol. 13487, pp. 50\u201366. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15008-1_5"},{"key":"32_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-030-99524-9_23","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Chakarov","year":"2022","unstructured":"Chakarov, A., Fedchin, A., Rakamari\u0107, Z., Rungta, N.: Better counterexamples for Dafny. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 404\u2013411. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_23"},{"key":"32_CR8","doi-asserted-by":"publisher","unstructured":"Chen, T., et al.: Towards saving money in using smart contracts. In: Zisman, A., Apel, S. (eds.) Proceedings of the 40th International Conference on Software Engineering: New Ideas and Emerging Results, ICSE (NIER) 2018, Gothenburg, Sweden, 27 May\u201303 June 2018, pp. 81\u201384. ACM (2018). https:\/\/doi.org\/10.1145\/3183399.3183420","DOI":"10.1145\/3183399.3183420"},{"key":"32_CR9","doi-asserted-by":"publisher","unstructured":"Genet, T., Jensen, T.P., Sauvage, J.: Termination of Ethereum\u2019s smart contracts. In: Samarati, P., di Vimercati, S.D.C., Obaidat, M.S., Ben-Othman, J. (eds.) Proceedings of the 17th International Joint Conference on e-Business and Telecommunications, ICETE 2020 - Volume 2: SECRYPT, Lieusaint, Paris, France, 8\u201310 July 2020, pp. 39\u201351. ScitePress (2020). https:\/\/doi.org\/10.5220\/0009564100390051","DOI":"10.5220\/0009564100390051"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-89722-6_10","volume-title":"Principles of Security and Trust","author":"I Grishchenko","year":"2018","unstructured":"Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of Ethereum smart contracts. In: Bauer, L., K\u00fcsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 243\u2013269. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89722-6_10"},{"key":"32_CR11","unstructured":"Guido, D.: Episode 6: What the hell are the blockchain people doing, and why isn\u2019t it a dumpster fire? (2021). https:\/\/galois.com\/blog\/2020\/11\/introducing-the-building-better-systems-podcast\/. In Building Better Systems (podcast), Joey Dodds, Shpat Morina, Galois"},{"key":"32_CR12","doi-asserted-by":"publisher","unstructured":"Hildenbrandt, E., et al.: KEVM: a complete formal semantics of the Ethereum virtual machine. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, 9\u201312 July 2018, pp. 204\u2013217. IEEE Computer Society (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00022","DOI":"10.1109\/CSF.2018.00022"},{"key":"32_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1007\/978-3-319-70278-0_33","volume-title":"Financial Cryptography and Data Security","author":"Y Hirai","year":"2017","unstructured":"Hirai, Y.: Defining the Ethereum virtual machine for interactive theorem provers. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 520\u2013535. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70278-0_33"},{"key":"32_CR14","unstructured":"Jackson, D., Nandi, C., Sagiv, M.: Certora technology white paper. Medium Post (2022). https:\/\/medium.com\/certora\/certora-technology-white-paper-cae5ab0bdf1"},{"key":"32_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-50497-0","volume-title":"Decision Procedures - An Algorithmic Point of View","author":"D Kroening","year":"2016","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View, 2nd edn. Springer, Heidelberg (2016)","edition":"2"},{"key":"32_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-19861-8_3","volume-title":"Compiler Construction","author":"N Lameed","year":"2011","unstructured":"Lameed, N., Hendren, L.: Staged static techniques to efficiently implement array copy semantics in a MATLAB JIT compiler. In: Knoop, J. (ed.) CC 2011. LNCS, vol. 6601, pp. 22\u201341. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19861-8_3"},{"issue":"4","key":"32_CR17","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363\u2013446 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9155-4","journal-title":"J. Autom. Reason."},{"key":"32_CR18","doi-asserted-by":"publisher","unstructured":"Mulligan, D.P., Owens, S., Gray, K.E., Ridge, T., Sewell, P.: Lem: reusable engineering of real-world semantics. In: Jeuring, J., Chakravarty, M.M.T. (eds.) Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, 1\u20133 September 2014, pp. 175\u2013188. ACM (2014). https:\/\/doi.org\/10.1145\/2628136.2628143","DOI":"10.1145\/2628136.2628143"},{"key":"32_CR19","doi-asserted-by":"crossref","unstructured":"Odersky, M.: How to make destructive updates less destructive. In: Proceedings of the ACM Symposium on the Principles of Programming Languages (POPL), pp. 25\u201336 (1991)","DOI":"10.1145\/99583.99590"},{"key":"32_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-030-53288-8_8","volume-title":"Computer Aided Verification","author":"D Park","year":"2020","unstructured":"Park, D., Zhang, Y., Rosu, G.: End-to-end formal verification of Ethereum 2.0 deposit smart contract. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 151\u2013164. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_8"},{"key":"32_CR21","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1016\/j.scico.2015.09.006","volume":"113","author":"DJ Pearce","year":"2015","unstructured":"Pearce, D.J., Groves, L.: Designing a verifying compiler: lessons learned from developing Whiley. Sci. Comput. Program. 113, 191\u2013220 (2015)","journal-title":"Sci. Comput. Program."},{"key":"32_CR22","doi-asserted-by":"crossref","unstructured":"Racordon, D., Shabalin, D., Zheng, D., Abrahams, D., Saeta, B.: Implementation strategies for mutable value semantics. J. Object Technol. 21(2) (2022)","DOI":"10.5381\/jot.2022.21.2.a2"},{"key":"32_CR23","doi-asserted-by":"publisher","unstructured":"Rosu, G.: $$\\mathbb{K}$$: a semantic framework for programming languages and formal analysis tools. In: Pretschner, A., Peled, D., Hutzelmann, T. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 50, pp. 186\u2013206. IOS Press (2017). https:\/\/doi.org\/10.3233\/978-1-61499-810-5-186","DOI":"10.3233\/978-1-61499-810-5-186"},{"key":"32_CR24","unstructured":"Runtime Verification: The IELE virtual machine. Blog post (2022). https:\/\/runtimeverification.com\/the-iele-virtual-machine\/"},{"key":"32_CR25","doi-asserted-by":"publisher","unstructured":"Schneidewind, C., Grishchenko, I., Scherer, M., Maffei, M.: eThor: practical and provably sound static analysis of Ethereum smart contracts. In: Ligatti, J., Ou, X., Katz, J., Vigna, G. (eds.) 2020 ACM SIGSAC Conference on Computer and Communications Security, CCS 2020, Virtual Event, USA, 9\u201313 November 2020, pp. 621\u2013640. ACM (2020). https:\/\/doi.org\/10.1145\/3372297.3417250","DOI":"10.1145\/3372297.3417250"},{"key":"32_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45607-4_1","volume-title":"Logic Based Program Synthesis and Transformation","author":"N Shankar","year":"2002","unstructured":"Shankar, N.: Static analysis for safe destructive updates in a functional language. In: Pettorossi, A. (ed.) LOPSTR 2001. LNCS, vol. 2372, pp. 1\u201324. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45607-4_1"},{"key":"32_CR27","unstructured":"Trail of Bits: Rattle - an Ethereum EVM binary analysis framework. Medium Post (2018). https:\/\/blog.trailofbits.com\/2018\/09\/06\/rattle-an-ethereum-evm-binary-analysis-framework\/"},{"key":"32_CR28","unstructured":"Wood, G.: Ethereum: a secure decentralised generalised transaction ledger. Ethereum project yellow paper (2022). https:\/\/ethereum.github.io\/yellowpaper\/paper.pdf. Berlin version d77a387. Accessed 26 Apr 2022"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-27481-7_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,2]],"date-time":"2023-03-02T14:11:51Z","timestamp":1677766311000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-27481-7_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031274800","9783031274817"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-27481-7_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"3 March 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"L\u00fcbeck","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":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 March 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 March 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fm2023.isp.uni-luebeck.de\/wordpress\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"95","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The proceedings also include 7 short industry papers","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}