{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:25:37Z","timestamp":1779074737038,"version":"3.51.4"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031773815","type":"print"},{"value":"9783031773822","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,26]],"date-time":"2024-11-26T00:00:00Z","timestamp":1732579200000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-77382-2_19","type":"book-chapter","created":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T19:26:56Z","timestamp":1732562816000},"page":"328-346","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["An Operational Semantics for\u00a0Yul"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3970-2486","authenticated-orcid":false,"given":"Vasileios","family":"Koutavas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5783-9454","authenticated-orcid":false,"given":"Yu-Yang","family":"Lin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8509-8059","authenticated-orcid":false,"given":"Nikos","family":"Tzevelekos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,26]]},"reference":[{"key":"19_CR1","unstructured":"Smart Contract Vulnerabilities (SCV) list. https:\/\/github.com\/sirhashalot\/SCV-List. Accessed 6 June 2024"},{"key":"19_CR2","unstructured":"Oyente, March 2017. https:\/\/github.com\/enzymefinance\/oyente\/releases\/tag\/0.2.7"},{"key":"19_CR3","unstructured":"Yul-Isabelle: Executable formal semantics of Yul (2021). https:\/\/github.com\/mmalvarez\/Yul-Isabelle\/tree\/master. Accessed 24 June 2024"},{"key":"19_CR4","unstructured":"Manticore, February 2022. https:\/\/github.com\/trailofbits\/manticore\/releases\/tag\/0.3.7"},{"key":"19_CR5","unstructured":"Echidna, March 2024. https:\/\/github.com\/crytic\/echidna\/releases\/tag\/v2.2.3"},{"key":"19_CR6","unstructured":"Gambit: Mutant generation for Solidity, May 2024. https:\/\/github.com\/Certora\/gambit\/releases\/tag\/v1.0.5"},{"key":"19_CR7","unstructured":"Mythril, March 2024. https:\/\/github.com\/Consensys\/mythril\/releases\/tag\/v0.24.8"},{"key":"19_CR8","unstructured":"Slither, June 2024. https:\/\/github.com\/crytic\/slither\/releases\/tag\/0.10.3"},{"key":"19_CR9","unstructured":"Solhint, May 2024. https:\/\/github.com\/protofire\/solhint\/releases\/tag\/v5.0.1"},{"key":"19_CR10","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS 2016, pp. 91\u201396. Association for Computing Machinery, New York, NY, USA (2016). https:\/\/doi.org\/10.1145\/2993600.2993611","DOI":"10.1145\/2993600.2993611"},{"key":"19_CR11","unstructured":"Cassez, F.: Formal and executable semantics of Yul in Dafny, October 2023. https:\/\/hackmd.io\/@FranckC\/BJz02K4Za. Accessed 24 June 2024"},{"key":"19_CR12","unstructured":"Cassez, F.: yul-dafny, October 2023. https:\/\/github.com\/franck44\/yul-dafny. Accessed 24 June 2024"},{"key":"19_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1007\/978-3-031-27481-7_32","volume-title":"FM 2023","author":"F Cassez","year":"2023","unstructured":"Cassez, F., Fuller, J., Ghale, M.K., Pearce, D.J., Quiles, H.M.A.: Formal and executable semantics of the Ethereum virtual machine in Dafny. In: Chechik, M., Katoen, J.P., Leucker, M. (eds.) FM 2023. LNCS, vol. 14000, pp. 571\u2013583. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-27481-7_32"},{"key":"19_CR14","unstructured":"Crosara, M., Centurino, G., Arceri, V.: Towards an operational semantics for Solidity (2019). https:\/\/api.semanticscholar.org\/CorpusID:249983842"},{"key":"19_CR15","unstructured":"Crystal Intelligence: Adolescent anarchy: Thirteen years of crypto crimes unveiled. https:\/\/crystalintelligence.com\/rohirov\/2024\/06\/Crystal-Intelligence-Thirteen-Years-of-Crypto-Crimes-Unveiled.pdf. Accessed 25 June 2024"},{"key":"19_CR16","unstructured":"ethereum.org: Ethereum execution client specifications. https:\/\/github.com\/ethereum\/execution-specs.git. Accessed 14 June 2024"},{"key":"19_CR17","unstructured":"ethereum.org: The Solidity contract-oriented programming language. https:\/\/github.com\/ethereum\/solidity.git. Accessed 13 June 2024"},{"key":"19_CR18","unstructured":"ethereum.org: Yul-K (2019). https:\/\/github.com\/ethereum\/Yul-K. Accessed 24 June 2024"},{"key":"19_CR19","doi-asserted-by":"publisher","unstructured":"Feist, J., Greico, G., Groce, A.: Slither: a static analysis framework for smart contracts (2019). https:\/\/doi.org\/10.1109\/WETSEB.2019.00008","DOI":"10.1109\/WETSEB.2019.00008"},{"key":"19_CR20","unstructured":"Felleisen, M., Friedman, D.P.: Control operators, the SECD-machine, and the $$\\lambda $$-calculus. In: Wirsing, M. (ed.) Formal Description of Programming Concepts - III: Proceedings of the IFIP TC 2\/WG 2.2 Working Conference on Formal Description of Programming Concepts - III, Ebberup, Denmark, 25\u201328 August 1986, pp. 193\u2013222. North-Holland (1987)"},{"key":"19_CR21","doi-asserted-by":"publisher","unstructured":"Grech, N., Lagouvardos, S., Tsatiris, I., Smaragdakis, Y.: Elipmoc: advanced decompilation of Ethereum smart contracts. Proc. ACM Program. Lang. 6(OOPSLA1) (2022). https:\/\/doi.org\/10.1145\/3527321","DOI":"10.1145\/3527321"},{"key":"19_CR22","doi-asserted-by":"publisher","unstructured":"Grieco, G., Song, W., Cygan, A., Feist, J., Groce, A.: Echidna: effective, usable, and fast fuzzing for smart contracts, pp. 557\u2013560 (2020). https:\/\/doi.org\/10.1145\/3395363.3404366","DOI":"10.1145\/3395363.3404366"},{"key":"19_CR23","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":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-030-44914-8_9","volume-title":"Programming Languages and Systems","author":"\u00c1 Hajdu","year":"2020","unstructured":"Hajdu, \u00c1., Jovanovi\u0107, D.: SMT-friendly formalization of the Solidity memory model. In: ESOP 2020. LNCS, vol. 12075, pp. 224\u2013250. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-44914-8_9"},{"key":"19_CR25","unstructured":"Kestrel Institute: Yul directory, Kestrel Books in ACL2 repository (2023). https:\/\/github.com\/acl2\/acl2\/tree\/master\/books\/kestrel\/yul. Accessed 24 June 2024"},{"key":"19_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-030-99527-0_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Koutavas","year":"2022","unstructured":"Koutavas, V., Lin, Y.-Y., Tzevelekos, N.: From bounded checking to verification of equivalence via symbolic up-to techniques. In: TACAS 2022. LNCS, vol. 13244, pp. 178\u2013195. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_10"},{"key":"19_CR27","doi-asserted-by":"publisher","unstructured":"Lin, Y.Y.: LaifsV1\/YulTracer: alpha 0.1.1: parametric parser and main, June 2024. https:\/\/doi.org\/10.5281\/zenodo.12511493","DOI":"10.5281\/zenodo.12511493"},{"key":"19_CR28","doi-asserted-by":"publisher","unstructured":"Lin, Y.Y.: Yultracer: Alpha 0.1.1 (artefact), June 2024. https:\/\/doi.org\/10.5281\/zenodo.12588076","DOI":"10.5281\/zenodo.12588076"},{"key":"19_CR29","unstructured":"Lin, Y., Tzevelekos, N.: Symbolic execution game semantics. In: FSCD. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"19_CR30","doi-asserted-by":"publisher","unstructured":"Luu, L., Chu, D., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Weippl, E.R., Katzenbeisser, S., Kruegel, C., Myers, A.C., Halevi, S. (eds.) Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, 24\u201328 October 2016, pp. 254\u2013269. ACM (2016). https:\/\/doi.org\/10.1145\/2976749.2978309","DOI":"10.1145\/2976749.2978309"},{"key":"19_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-030-92124-8_23","volume-title":"Software Engineering and Formal Methods","author":"D Marmsoler","year":"2021","unstructured":"Marmsoler, D., Brucker, A.D.: A denotational semantics of\u00a0Solidity in\u00a0Isabelle\/HOL. In: Calinescu, R., P\u0103s\u0103reanu, C.S. (eds.) SEFM 2021. LNCS, vol. 13085, pp. 403\u2013422. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-92124-8_23"},{"key":"19_CR32","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-031-47115-5_11","volume-title":"SEFM 2023","author":"D Marmsoler","year":"2023","unstructured":"Marmsoler, D., Thornton, B.: SSCalc: a calculus for Solidity smart contracts. In: Ferreira, C., Willemse, T.A.C. (eds.) SEFM 2023. LNCS, vol. 14323, pp. 184\u2013204. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-47115-5_11"},{"key":"19_CR33","doi-asserted-by":"publisher","unstructured":"Mossberg, M., et al.: Manticore: a user-friendly symbolic execution framework for binaries and smart contracts, pp. 1186\u20131189 (2019). https:\/\/doi.org\/10.1109\/ASE.2019.00133","DOI":"10.1109\/ASE.2019.00133"},{"key":"19_CR34","unstructured":"NethermindEth: Yul IR specification in Lean (2021). https:\/\/github.com\/NethermindEth\/Yul-Specification. Accessed 24 June 2024"},{"key":"19_CR35","unstructured":"Peyton Jones, S.: System FC, as implemented in GHC (May). https:\/\/gitlab.haskell.org\/ghc\/ghc\/-\/blob\/master\/docs\/core-spec\/core-spec.pdf. Accessed 27 June 2024"},{"key":"19_CR36","unstructured":"Sharma, N., Sharma, S.: A survey of Mythril, a smart contract security analysis tool for EVM bytecode 13, 51003\u201351010 (2022)"},{"key":"19_CR37","unstructured":"Solidity Team: List of known bugs - Solidity 0.8.27 documentation. https:\/\/docs.soliditylang.org\/en\/develop\/bugs.html. Accessed 6 June 2024"},{"key":"19_CR38","unstructured":"Solidity Team: Yul - Solidity 0.8.27 documentation. https:\/\/docs.soliditylang.org\/en\/latest\/yul.html. Accessed 6 June 2024"},{"key":"19_CR39","doi-asserted-by":"crossref","unstructured":"Sulzmann, M., Chakravarty, M., Peyton\u00a0Jones, S., Donnelly, K.: System F with type equality coercions. In: ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI 2007), pp. 53\u201366. ACM, January 2007. https:\/\/www.microsoft.com\/en-us\/research\/publication\/system-f-with-type-equality-coercions\/","DOI":"10.1145\/1190315.1190324"},{"key":"19_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-030-03592-1_13","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"J Zakrzewski","year":"2018","unstructured":"Zakrzewski, J.: Towards verification of Ethereum smart contracts: a formalization of core of Solidity. In: Piskac, R., R\u00fcmmer, P. (eds.) VSTTE 2018. LNCS, vol. 11294, pp. 229\u2013247. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03592-1_13"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-77382-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,25]],"date-time":"2024-11-25T20:03:25Z","timestamp":1732565005000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-77382-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,26]]},"ISBN":["9783031773815","9783031773822"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-77382-2_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,11,26]]},"assertion":[{"value":"26 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Aveiro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}