{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T15:40:14Z","timestamp":1767195614130,"version":"3.48.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032104434"},{"type":"electronic","value":"9783032104441"}],"license":[{"start":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T00:00:00Z","timestamp":1762905600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T00:00:00Z","timestamp":1762905600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-10444-1_1","type":"book-chapter","created":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T06:58:50Z","timestamp":1762844330000},"page":"3-11","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Securely Optimized (Ethereum) Smart Contracts Using Formal Methods"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0048-0705","authenticated-orcid":false,"given":"Elvira","family":"Albert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samir","family":"Genaim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6189-4667","authenticated-orcid":false,"given":"Pablo","family":"Gordillo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2109-8863","authenticated-orcid":false,"given":"Alejandro","family":"Hern\u00e1ndez-Cerezo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrique","family":"Martin Martin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0501-9830","authenticated-orcid":false,"given":"Albert","family":"Rubio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,12]]},"reference":[{"key":"1_CR1","unstructured":"Solidity Documentation (2025). https:\/\/docs.soliditylang.org\/en\/latest\/index.html"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Ara\u00fajo Aguiar, M., et al.: Neural-guided superoptimization in Ethereum. Inf. Softw. Technol. 186, 107800 (2025)","DOI":"10.1016\/j.infsof.2025.107800"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Albert, E., Correas, J., Gordillo, P., Rom\u00e1n-D\u00edez, G., Rubio, A.: Inferring needless write memory accesses on Ethereum bytecode. In: Sankaranarayanan, S., Sharygina, N., (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part I, vol. 13993 of LNCS, pp. 448\u2013466. Springer (2023)","DOI":"10.1007\/978-3-031-30823-9_23"},{"key":"1_CR4","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2024.112284","volume":"221","author":"E Albert","year":"2025","unstructured":"Albert, E., Correas, J., Gordillo, P., Rom\u00e1n-D\u00edez, G., Rubio, A.: Harnessing heap analysis for the synthesis of superoptimized bytecode. J. Syst. Softw. 221, 112284 (2025)","journal-title":"J. Syst. Softw."},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Albert, E., et al.: SuperStack: superoptimization of stack-bytecode via greedy, constraint-based, and SAT techniques. Proc. ACM Program. Lang. 8(PLDI), 1437\u20131462 (2024)","DOI":"10.1145\/3656435"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Albert, E., Genaim, S., Kirchner, D., Martin-Martin, E.: Formally verified EVM block-optimizations. In: Computer Aided Verification - 35th International Conference, CAV 2023, Paris, France, July 17-22, 2023, Proceedings, Part III, vol. 13966 of Lecture Notes in Computer Science, pp. 176\u2013189. Springer (2023)","DOI":"10.1007\/978-3-031-37709-9_9"},{"issue":"4","key":"1_CR7","doi-asserted-by":"publisher","first-page":"3676","DOI":"10.1109\/TDSC.2025.3536803","volume":"22","author":"E Albert","year":"2025","unstructured":"Albert, E., Genaim, S., Kirchner, D., Martin-Martin, E.: Secure optimizations on Ethereum bytecode jump-free sequences. IEEE Trans. Depend. Sec. Comput. 22(4), 3676\u20133691 (2025)","journal-title":"IEEE Trans. Depend. Sec. Comput."},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Albert, E., Gordillo, P., Hern\u00e1ndez-Cerezo, A., Rubio, A.: A max-SMT superoptimizer for EVM handling Memory and Storage. In: Fisman, D., Rosu, G., (eds.,) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, pp. 201\u2013219. Springer (2022)","DOI":"10.1007\/978-3-030-99524-9_11"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Albert, E., Gordillo, P., Hern\u00e1ndez-Cerezo, A., Rubio, A., Schett, M.A.: Super-optimization of smart contracts. ACM Trans. Softw. Eng. Methodol. 31(4), 70:1\u201370:29 (2022)","DOI":"10.1145\/3506800"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-030-53288-8_10","volume-title":"Computer Aided Verification","author":"E Albert","year":"2020","unstructured":"Albert, E., Gordillo, P., Rubio, A., Schett, M.A.: Synthesis of super-optimized smart contracts using max-SMT. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 177\u2013200. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_10"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Bacchus, F., J\u00e4rvisalo, M., Martins, R.: Maximum satisfiability. In: Handbook of Satisfiability, pp. 929\u2013991. IOS Press (2021)","DOI":"10.3233\/FAIA201008"},{"key":"1_CR12","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions","author":"Y Bertot","year":"2010","unstructured":"Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions, 1st edn. Springer Publishing Company, Incorporated (2010)","edition":"1"},{"key":"1_CR13","unstructured":"Coq Development Team. The Coq Proof Assistant Reference Manual - Version 8.20.0. https:\/\/rocq-prover.org\/doc\/V8.20.0\/refman\/ (2024)"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura, L., Kong, S., Avigad, J., Doorn, F.V., Raumer, J.V.: The lean theorem prover (system description). In: International Conference on Automated Deduction, pp. 378\u2013388. Springer (2015)","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Forster, Y., Sozeau, M., Tabareau, N.: Verified extraction from Coq to OCaml. Proc. ACM Program. Lang. 8(PLDI) (2024)","DOI":"10.1145\/3656379"},{"issue":"8","key":"1_CR16","doi-asserted-by":"publisher","first-page":"1735","DOI":"10.1162\/neco.1997.9.8.1735","volume":"9","author":"S Hochreiter","year":"1997","unstructured":"Hochreiter, S., Schmidhuber, J.: Long short-term memory. Neural Comput. 9(8), 1735\u20131780 (1997)","journal-title":"Neural Comput."},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Jangda, A., Yorsh, G.: Unbounded superoptimization. In: Proceedings of the 2017 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2017, Vancouver, BC, Canada, October 23 - 27, 2017, pp. 78\u201388 (2017)","DOI":"10.1145\/3133850.3133856"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Massalin, H.: Superoptimizer - a look at the smallest program. In: Proceedings of the Second International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS II), pp. 122\u2013126 (1987)","DOI":"10.1145\/36206.36194"},{"key":"1_CR19","volume-title":"Foundations of Machine Learning","author":"M Mohri","year":"2012","unstructured":"Mohri, M., Rostamizadeh, A., Talwalkar, A.: Foundations of Machine Learning. MIT Press, Adaptive computation and machine learning (2012)"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"de Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: International Conference on Automated Deduction, pp. 625\u2013635. Springer (2021)","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Mesnard, F., Stuckey, P.J. (eds.): LOPSTR 2018. LNCS, vol. 11408. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-13838-7","DOI":"10.1007\/978-3-030-13838-7"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Programming and proving in Isabelle\/HOL. https:\/\/isabelle.in.tum.de\/dist\/Isabelle2025\/doc\/prog-prove.pdf (2013)","DOI":"10.1007\/978-3-319-10542-0_6"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Klein, G.: Concrete semantics: with Isabelle\/HOL. Springer (2014)","DOI":"10.1007\/978-3-319-10542-0"},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Sergey, I.: Programs and Proofs: Mechanizing Mathematics with Dependent Types (2014). https:\/\/doi.org\/10.5281\/zenodo.4996238","DOI":"10.5281\/zenodo.4996238"},{"key":"1_CR26","unstructured":"The\u00a0PyTorch Team. PyTorch. http:\/\/pytocrh.org"},{"key":"1_CR27","unstructured":"Ashish Vaswani, et al.: Attention is all you need. In: Guyon, I., et al. (eds.) Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA, pp. 5998\u20136008 (2017)"},{"key":"1_CR28","unstructured":"Wood, G.: Ethereum: A Secure Decentralised Generalised Transaction Ledger (2019)"}],"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-032-10444-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T15:35:52Z","timestamp":1767195352000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-10444-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,12]]},"ISBN":["9783032104434","9783032104441"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-10444-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,11,12]]},"assertion":[{"value":"12 November 2025","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":"Toledo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","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 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 November 2025","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":"sefm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sefm-conference.github.io\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}