{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,16]],"date-time":"2026-09-16T16:52:57Z","timestamp":1789577577315,"version":"build-2803163510"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2022,7,12]],"date-time":"2022-07-12T00:00:00Z","timestamp":1657584000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Spanish","award":["MCIN\/AEI\/10.13039\/501100011033\/FEDER"],"award-info":[{"award-number":["MCIN\/AEI\/10.13039\/501100011033\/FEDER"]}]},{"name":"Una manera de hacer Europa","award":["RTI2018-094403-B-C31 and RTI2018-094403-B-C33"],"award-info":[{"award-number":["RTI2018-094403-B-C31 and RTI2018-094403-B-C33"]}]},{"name":"CM project","award":["S2018\/TCS-4314"],"award-info":[{"award-number":["S2018\/TCS-4314"]}]},{"DOI":"10.13039\/501100015595","name":"Ethereum Foundation","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100015595","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>\n            Smart contracts are programs deployed on a blockchain. They are executed for a monetary fee paid in\n            <jats:italic>gas<\/jats:italic>\n            \u2014a clear optimization target for smart contract compilers. Because smart contracts are a young, fast-moving field without (manually) fine-tuned compilers, they highly benefit from automated and adaptable approaches, especially as smart contracts are effectively immutable, and as such need a high level of assurance. This makes them an ideal domain for applying formal methods. Super-optimization is a technique to find the best translation of a block of instructions by trying all possible sequences of instructions that produce the same result. We present a framework for super-optimizing smart contracts based on Max-SMT with two main ingredients: (1) a\n            <jats:italic>stack functional specification<\/jats:italic>\n            extracted from the basic blocks of a smart contract, which is simplified using rules capturing the semantics of arithmetic, bit-wise, and relational operations, and (2) the\n            <jats:italic>synthesis of optimized blocks<\/jats:italic>\n            , which finds\u2014by means of an efficient SMT encoding\u2014basic blocks with minimal gas cost whose stack functional specification is equal (modulo commutativity) to the extracted one.\n          <\/jats:p>\n          <jats:p>\n            We implemented our framework in the tool\n            <jats:sans-serif>syrup\u00a02.0<\/jats:sans-serif>\n            . Through large-scale experiments on real-world smart contracts, we analyze performance improvements for different SMT encodings, as well as tradeoffs between quality of optimizations and required optimization time.\n          <\/jats:p>","DOI":"10.1145\/3506800","type":"journal-article","created":{"date-parts":[[2022,4,23]],"date-time":"2022-04-23T11:22:32Z","timestamp":1650712952000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Super-optimization of Smart Contracts"],"prefix":"10.1145","volume":"31","author":[{"given":"Elvira","family":"Albert","sequence":"first","affiliation":[{"name":"Complutense University of Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6189-4667","authenticated-orcid":false,"given":"Pablo","family":"Gordillo","sequence":"additional","affiliation":[{"name":"Complutense University of Madrid, Spain"}],"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":[{"name":"Complutense University of Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Albert","family":"Rubio","sequence":"additional","affiliation":[{"name":"Complutense University of Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Maria A.","family":"Schett","sequence":"additional","affiliation":[{"name":"University College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,7,12]]},"reference":[{"key":"e_1_3_3_2_2","unstructured":"2018. Etherscan. https:\/\/etherscan.io."},{"key":"e_1_3_3_3_2","unstructured":"2018. Rattle - An EVM Binary Static Analysis Framework. https:\/\/github.com\/crytic\/rattle."},{"key":"e_1_3_3_4_2","unstructured":"Ethereum. 2021. Solidity documentation. https:\/\/docs.soliditylang.org\/en\/latest\/index.html."},{"key":"e_1_3_3_5_2","unstructured":"Ethereum. 2021. Yul documentation. https:\/\/docs.soliditylang.org\/en\/latest\/yul.html."},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_7"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2021.110923"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_30"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_10"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_27"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/11799573_21"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/Blockchain50366.2020.00042"},{"key":"e_1_3_3_13_2","first-page":"442","volume-title":"SANER","author":"Chen Ting","year":"2017","unstructured":"Ting Chen, Xiaoqi Li, Xiapu Luo, and Xiaosong Zhang. 2017. Under-optimized smart contracts devour your money. In SANER. IEEE Computer Society, 442\u2013446."},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3183399.3183420"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_3_17_2","unstructured":"Ethereum. 2018. Solidity. https:\/\/solidity.readthedocs.io."},{"key":"e_1_3_3_18_2","unstructured":"L. M. Goodman. 2014. Tezos: A Self-Amending Crypto-Ledger Position Paper. (2014) 18."},{"key":"e_1_3_3_19_2","first-page":"116:1\u2013116:27","article-title":"MadMax: Surviving out-of-gas conditions in Ethereum smart contracts","volume":"2","author":"Grech Neville","year":"2018","unstructured":"Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis. 2018. MadMax: Surviving out-of-gas conditions in Ethereum smart contracts. PACMPL 2, OOPSLA (2018), 116:1\u2013116:27.","journal-title":"PACMPL"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133850.3133856"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3278532.3278575"},{"key":"e_1_3_3_22_2","unstructured":"Nomadic Labs. 2018. Michelson: The Language of Smart Contracts in Tezos. https:\/\/www.michelson-lang.com."},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3166064"},{"key":"e_1_3_3_25_2","first-page":"254","volume-title":"CCS","author":"Luu Loi","year":"2016","unstructured":"Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016. Making smart contracts smarter. In CCS. ACM, 254\u2013269."},{"key":"e_1_3_3_26_2","first-page":"122","volume-title":"Proceedings of the 2nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS II\u201987)","author":"Massalin Henry","year":"1987","unstructured":"Henry Massalin. 1987. Superoptimizer - A look at the smallest program. In Proceedings of the 2nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS II\u201987). 122\u2013126. https:\/\/dl.acm.org\/citation.cfm?id=36194."},{"key":"e_1_3_3_27_2","unstructured":"Libra Association Members. 2019. White paper: The Libra Blockchain. 29."},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.225"},{"key":"e_1_3_3_29_2","volume-title":"The 9th Annual HITB Security Conference","author":"Mueller Bernhard","year":"2018","unstructured":"Bernhard Mueller. 2018. Smashing Ethereum smart contracts for fun and real profit. In The 9th Annual HITB Security Conference."},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428245"},{"key":"e_1_3_3_31_2","volume-title":"Ethereum Smart Contract Development","author":"Mukhopadhyay Mayukh","year":"2018","unstructured":"Mayukh Mukhopadhyay. 2018. Ethereum Smart Contract Development. Packt Publishing."},{"key":"e_1_3_3_32_2","volume-title":"Preproceedings of 29th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR\u201919)","author":"Nagele Julian","year":"2019","unstructured":"Julian Nagele and Maria A. Schett. 2019. Blockchain superoptimizer. In Preproceedings of 29th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR\u201919). https:\/\/arxiv.org\/abs\/2005.05912."},{"key":"e_1_3_3_33_2","unstructured":"Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system."},{"key":"e_1_3_3_34_2","article-title":"Broken metre: Attacking resource metering in EVM","volume":"1909","author":"P\u00e9rez Daniel","year":"2019","unstructured":"Daniel P\u00e9rez and Benjamin Livshits. 2019. Broken metre: Attacking resource metering in EVM. CoRR abs\/1909.07220 (2019). arxiv:1909.07220http:\/\/arxiv.org\/abs\/1909.07220.","journal-title":"CoRR"},{"key":"e_1_3_3_35_2","article-title":"Souper: A synthesizing superoptimizer","author":"Sasnauskas Raimondas","year":"2017","unstructured":"Raimondas Sasnauskas, Yang Chen, Peter Collingbourne, Jeroen Ketema, Gratian Lup, Jubi Taneja, and John Regehr. 2017. Souper: A synthesizing superoptimizer. arXiv:1711.04422 [cs] (Nov. 2017). arxiv:1711.04422 [cs].","journal-title":"arXiv:1711.04422 [cs]"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.FMBC.2020.3"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360611"},{"key":"e_1_3_3_38_2","first-page":"27","volume-title":"Move: A Language With Programmable Resources","author":"Team The LibraBFT","year":"2020","unstructured":"The LibraBFT Team. 2020. Move: A Language With Programmable Resources. Technical Report. Novi. 27 pages. https:\/\/developers.libra.org\/docs\/state-machine-replication-paper."},{"key":"e_1_3_3_39_2","unstructured":"Gavin Wood. 2019. Ethereum: A secure decentralised generalised transaction ledger."},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSPW.2019.00041"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3402450"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3506800","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3506800","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:31:09Z","timestamp":1750188669000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3506800"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,7,12]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3506800"],"URL":"https:\/\/doi.org\/10.1145\/3506800","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,7,12]]},"assertion":[{"value":"2021-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-12-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-07-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}