{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T20:17:49Z","timestamp":1767212269407,"version":"3.41.2"},"reference-count":47,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"4","license":[{"start":{"date-parts":[[2025,7,1]],"date-time":"2025-07-01T00:00:00Z","timestamp":1751328000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"Spanish MCI, AEI and FEDER (EU) project","award":["PID2021-122830OB-C41","TEC-2024\/COM-235"],"award-info":[{"award-number":["PID2021-122830OB-C41","TEC-2024\/COM-235"]}]},{"name":"Ethereum Foundation FORVES","award":["FY22-0698","AOC-1661"],"award-info":[{"award-number":["FY22-0698","AOC-1661"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Dependable and Secure Comput."],"published-print":{"date-parts":[[2025,7]]},"DOI":"10.1109\/tdsc.2025.3536803","type":"journal-article","created":{"date-parts":[[2025,2,3]],"date-time":"2025-02-03T13:34:23Z","timestamp":1738589663000},"page":"3676-3691","source":"Crossref","is-referenced-by-count":2,"title":["Secure Optimizations on Ethereum Bytecode Jump-Free Sequences"],"prefix":"10.1109","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0048-0705","authenticated-orcid":false,"given":"Elvira","family":"Albert","sequence":"first","affiliation":[{"name":"Department of Computer Systems and Computing, Complutense University of Madrid, Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7176-1881","authenticated-orcid":false,"given":"Samir","family":"Genaim","sequence":"additional","affiliation":[{"name":"Department of Computer Systems and Computing, Complutense University of Madrid, Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9229-1148","authenticated-orcid":false,"given":"Daniel","family":"Kirchner","sequence":"additional","affiliation":[{"name":"Ethereum Foundation, Zug, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1664-018X","authenticated-orcid":false,"given":"Enrique","family":"Martin-Martin","sequence":"additional","affiliation":[{"name":"Department of Computer Systems and Computing, Complutense University of Madrid, Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168906"},{"key":"ref2","first-page":"122","article-title":"Superoptimizer - A look at the smallest program","volume-title":"Proc. 2nd Int. Conf. Architectural Support Program. Lang. Operating Syst.","author":"Massalin"},{"key":"ref3","first-page":"177","article-title":"Binary translation using peephole superoptimizers","volume-title":"Proc. 8th USENIX Symp. Operating Syst. Des. Implementation","author":"Bansal"},{"key":"ref4","first-page":"166","article-title":"Blockchain superoptimizer","volume-title":"Proc. 29th Int. Symp. Log.-Based Prog. Synth. Transformation","author":"Nagele"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/3506800"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_11"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/3133850.3133856"},{"article-title":"Souper: A Synthesizing Superoptimizer","year":"2017","author":"Sasnauskas","key":"ref8"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"ref11","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","volume":"2283","author":"Nipkow","year":"2002"},{"article-title":"Analysis of the DAO exploit","year":"2016","author":"Daian","key":"ref12"},{"article-title":"Critical Update Re: DAO vulnerability","year":"2016","author":"Buterin","key":"ref13"},{"article-title":"Spankchain loses ${\\$}$$40k in hack due to smart contract bug","year":"2018","author":"Palmer","key":"ref14"},{"article-title":"imBTC uniswap pool drained for ${\\$}$$300k in ETH","year":"2020","author":"Turley","key":"ref15"},{"article-title":"A hackers\u2019 dream payday: Ledf.me and uniswap lose ${\\$}$$25 million worth of cryptocurrency","year":"2020","author":"Bizga","key":"ref16"},{"article-title":"Preventing reentrancy bugs - another use case for formal verification","year":"2020","author":"Bernardi","key":"ref17"},{"year":"2023","key":"ref18","article-title":"Certora"},{"year":"2023","key":"ref19","article-title":"Veridise"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_10"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/3656435"},{"year":"2021","key":"ref25","article-title":"The ${\\sf solc}$solc optimizer"},{"article-title":"Ethereum: A secure decentralised generalised transaction ledger (Berlin version 8fea825\u20132022\u201308-22)","year":"2022","author":"Wood","key":"ref26"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_9"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_9"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243780"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/3166064"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/bfb0040259"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70278-0_33"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/2692915.2628143"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/csf.2018.00022"},{"year":"2020","key":"ref35","article-title":"Coq formalisation of the ethereum virtual machine (WIP)"},{"year":"2018","key":"ref36","article-title":"Bedrock Bit Vectors (BBV)"},{"article-title":"Verification and certification of EVM optimizations","year":"2024","author":"Leal S\u00e1nchez","key":"ref37"},{"key":"ref38","first-page":"102","article-title":"A unit two variable per inequality integer constraint solver for constraint logic programming","volume-title":"Proc. Australian Comput. Sci. Conf.","author":"Harvey"},{"article-title":"Tightened transitive closure of integer addition constraints","volume-title":"Proc. 8th Symp. Abstraction, Reformulation, Approximation","author":"Revesz","key":"ref39"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328444"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46663-6_12"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/3428197"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503679"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/3434327"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/3461648.3463850"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/3529507"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542512"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706311"},{"article-title":"Certifying assembly optimizations in Coq by symbolic execution with hash-consing","volume-title":"Proc. Coq Workshop","author":"Gourdin","key":"ref51"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1145\/3622799"}],"container-title":["IEEE Transactions on Dependable and Secure Computing"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/8858\/11077775\/10870158.pdf?arnumber=10870158","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T22:48:32Z","timestamp":1752274112000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10870158\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7]]},"references-count":47,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.1109\/tdsc.2025.3536803","relation":{},"ISSN":["1545-5971","1941-0018","2160-9209"],"issn-type":[{"type":"print","value":"1545-5971"},{"type":"electronic","value":"1941-0018"},{"type":"electronic","value":"2160-9209"}],"subject":[],"published":{"date-parts":[[2025,7]]}}}