{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,9]],"date-time":"2026-10-09T01:21:57Z","timestamp":1791508917035,"version":"4.3.4"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030995232","type":"print"},{"value":"9783030995249","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Superoptimization is a compilation technique that searches for the optimal sequence of instructions semantically equivalent to a given (loop-free) initial sequence. With the advent of SMT solvers, it has been successfully applied to LLVM code (to reduce the number of instructions) and to Ethereum EVM bytecode (to reduce its gas consumption). Both applications, when proven practical, have left out memory operations and thus missed important optimization opportunities. A main challenge to superoptimization today is handling memory operations while remaining scalable. We present <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf {GASOL}^{v2}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msup>\n                    <mml:mi>GASOL<\/mml:mi>\n                    <mml:mrow>\n                      <mml:mi>v<\/mml:mi>\n                      <mml:mn>2<\/mml:mn>\n                    <\/mml:mrow>\n                  <\/mml:msup>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, a gas and bytes-size superoptimization tool for Ethereum smart contracts, that leverages a previous Max-SMT approach for only stack optimization to optimize also <jats:italic>wrt.<\/jats:italic> memory and storage. <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf {GASOL}^{v2}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msup>\n                    <mml:mi>GASOL<\/mml:mi>\n                    <mml:mrow>\n                      <mml:mi>v<\/mml:mi>\n                      <mml:mn>2<\/mml:mn>\n                    <\/mml:mrow>\n                  <\/mml:msup>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> can be used to optimize the size in bytes, aligned with the optimization criterion used by the Solidity compiler , and it can also be used to optimize gas consumption. Our experiments on 12,378 blocks from 30 randomly selected real contracts achieve gains of 16.42% in gas <jats:italic>wrt.<\/jats:italic> the previous version of the optimizer without memory handling, and gains of 3.28% in bytes-size over code already optimized by .<\/jats:p>","DOI":"10.1007\/978-3-030-99524-9_11","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:14:55Z","timestamp":1648534495000},"page":"201-219","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["A Max-SMT Superoptimizer for EVM handling Memory and Storage"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0048-0705","authenticated-orcid":false,"given":"Elvira","family":"Albert","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6189-4667","authenticated-orcid":false,"given":"Pablo","family":"Gordillo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2109-8863","authenticated-orcid":false,"given":"Alejandro","family":"Hern\u00e1ndez-Cerezo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0501-9830","authenticated-orcid":false,"given":"Albert","family":"Rubio","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"11_CR1","unstructured":"Compiler Input and Output JSON Description. https:\/\/docs.soliditylang.org\/en\/v0.8.7\/using-the-compiler.html#compiler-input-and-output-json-description."},{"key":"11_CR2","unstructured":"Welfare contract. https:\/\/etherscan.io\/address\/0x3E873439949793e8c577E08629c36Ed8c184e7D9#code."},{"key":"11_CR3","unstructured":"GASOL \u2013 A GAS Optimization tooLkit, 2021. Funded by the Ethereum Foundation https:\/\/blog.ethereum.org\/2021\/07\/01\/esp-allocation-update-q1-2021\/."},{"key":"11_CR4","unstructured":"The solc optimizer, 2021. https:\/\/docs.soliditylang.org\/en\/v0.8.7\/internals\/optimizer.html."},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Elvira Albert, Jes\u00fas Correas, Pablo Gordillo, Guillermo Rom\u00e1n-D\u00edez, and Albert Rubio. GASOL: Gas Analysis and Optimization for Ethereum Smart Contracts. In Armin Biere and David Parker, editors, Proceedings of 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020, volume 12079 of Lecture Notes in Computer Science, pages 118\u2013125, 2020.","DOI":"10.1007\/978-3-030-45237-7_7"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Elvira Albert, Jes\u00fas Correas, Pablo Gordillo, Guillermo Rom\u00e1n-D\u00edez, and Albert Rubio. Don\u2019t run on fumes\u2014parametric gas bounds for smart contracts. Journal of Systems and Software, 176:110923, 2021.","DOI":"10.1016\/j.jss.2021.110923"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Elvira Albert, Pablo Gordillo, Albert Rubio, and Maria A. Schett. Synthesis of super-optimized smart contracts using max-smt. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I, volume 12224 of Lecture Notes in Computer Science, pages 177\u2013200. Springer, 2020.","DOI":"10.1007\/978-3-030-53288-8_10"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Elvira Albert, Pablo Gordillo, Albert Rubio, and Ilya Sergey. Running on Fumes: Preventing Out-Of-Gas Vulnerabilities in Ethereum Smart Contracts using Static Resource Analysis. In 13th International Conference on Verification and Evaluation of Computer and Communication Systems, VECoS 2019. Proceedings, volume 11847 of LNCS, pages 63\u201378. Springer, 2019.","DOI":"10.1007\/978-3-030-35092-5_5"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Rajeev Alur, Rastislav Bod\u00edk, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, pages 1\u20138. IEEE, 2013.","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Sorav Bansal and Alex Aiken. Automatic generation of peephole superoptimizers. In John Paul Shen and Margaret Martonosi, editors, Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2006, San Jose, CA, USA, October 21-25, 2006, pages 394\u2013403. ACM, 2006.","DOI":"10.1145\/1168857.1168906"},{"key":"11_CR11","unstructured":"Sorav Bansal and Alex Aiken. Binary translation using peephole superoptimizers. In Richard Draves and Robbert van Renesse, editors, 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings, pages 177\u2013192. USENIX Association, 2008."},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. Optimizing synthesis with metasketches. In Rastislav Bod\u00edk and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 775\u2013788. ACM, 2016.","DOI":"10.1145\/2837614.2837666"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. The mathsat5 SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems - 19th International Conference, TACAS 2013. Proceedings, pages 93\u2013107, 2013.","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"F. Contro, M. Crosara, M. Ceccato, and M. Dalla Preda. Ethersolve: Computing an accurate control-flow graph from ethereum bytecode. In 29th IEEE\/ACM International Conference on Program Comprehension, ICPC 2021, Madrid, Spain, May 20-21, 2021, pages 127\u2013137. IEEE, 2021.","DOI":"10.1109\/ICPC52881.2021.00021"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Torbj\u00f6rn Granlund and Richard Kenner. Eliminating branches using a superoptimizer and the GNU C compiler. In Stuart I. Feldman and Richard L. Wexelblat, editors, Proceedings of the ACM SIGPLAN\u201992 Conference on Programming Language Design and Implementation (PLDI), San Francisco, California, USA, June 17-19, 1992, pages 341\u2013352. ACM, 1992.","DOI":"10.1145\/143095.143146"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis. MadMax: surviving out-of-gas conditions in Ethereum smart contracts. PACMPL, 2(OOPSLA):116:1\u2013116:27, 2018.","DOI":"10.1145\/3276486"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan. Synthesis of loop-free programs. In Mary W. Hall and David A. Padua, editors, Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, pages 62\u201373. ACM, 2011.","DOI":"10.1145\/1993498.1993506"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Abhinav Jangda and Greta Yorsh. 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, pages 78\u201388, 2017.","DOI":"10.1145\/3133850.3133856"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Matteo Marescotti, Martin Blicha, Antti E. J. Hyv\u00e4rinen, Sepideh Asadi, and Natasha Sharygina. Computing Exact Worst-Case Gas Consumption for Smart Contracts. In ISoLA, volume 11247 of LNCS, pages 450\u2013465. Springer, 2018.","DOI":"10.1007\/978-3-030-03427-6_33"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"Henry Massalin. 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), pages 122\u2013126, 1987.","DOI":"10.1145\/36204.36194"},{"key":"11_CR21","unstructured":"Julian Nagele and Maria A Schett. Blockchain superoptimizer. In Preproceedings of 29th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2019), 2019. https:\/\/arxiv.org\/abs\/2005.05912."},{"key":"11_CR22","unstructured":"Raimondas Sasnauskas, Yang Chen, Peter Collingbourne, Jeroen Ketema, Gratian Lup, Jubi Taneja, and John Regehr. Souper: A Synthesizing Superoptimizer. arXiv:1711.04422[cs], November 2017."},{"key":"11_CR23","unstructured":"Gavin Wood. Ethereum: A secure decentralised generalised transaction ledger, 2019."},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Renlord Yang, Toby Murray, Paul Rimba, and Udaya Parampalli. Empirically analyzing ethereum\u2019s gas mechanism. In 2019 IEEE European Symposium on Security and Privacy Workshops, EuroS&P Workshops 2019, Stockholm, Sweden, June 17-19, 2019, pages 310\u2013319, 2019.","DOI":"10.1109\/EuroSPW.2019.00041"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99524-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:20:01Z","timestamp":1648534801000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99524-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995232","9783030995249"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99524-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","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":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"159","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":"46","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":"4","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":"29% - 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":"10","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":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","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)"}}]}}