{"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":1789577577590,"version":"build-2803163510"},"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"],"award-info":[{"award-number":["PID2021-122830OB-C41"]}]},{"name":"Spanish MCI, AEI and FEDER (EU) project","award":["TEC-2024\/COM-235"],"award-info":[{"award-number":["TEC-2024\/COM-235"]}]},{"name":"Ethereum Foundation FORVES","award":["FY22-0698"],"award-info":[{"award-number":["FY22-0698"]}]},{"name":"Ethereum Foundation FORVES","award":["AOC-1661"],"award-info":[{"award-number":["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":3,"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9229-1148","authenticated-orcid":false,"given":"Daniel","family":"Kirchner","sequence":"additional","affiliation":[{"name":"Ethereum Foundation, Zug, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]}],"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"},{"key":"ref8","article-title":"Souper: A Synthesizing Superoptimizer","author":"Sasnauskas","year":"2017"},{"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"},{"key":"ref12","article-title":"Analysis of the DAO exploit","author":"Daian","year":"2016"},{"key":"ref13","article-title":"Critical Update Re: DAO vulnerability","author":"Buterin","year":"2016"},{"key":"ref14","article-title":"Spankchain loses ${\\$}$$40k in hack due to smart contract bug","author":"Palmer","year":"2018"},{"key":"ref15","article-title":"imBTC uniswap pool drained for ${\\$}$$300k in ETH","author":"Turley","year":"2020"},{"key":"ref16","article-title":"A hackers\u2019 dream payday: Ledf.me and uniswap lose ${\\$}$$25 million worth of cryptocurrency","author":"Bizga","year":"2020"},{"key":"ref17","article-title":"Preventing reentrancy bugs - another use case for formal verification","author":"Bernardi","year":"2020"},{"key":"ref18","article-title":"Certora","year":"2023"},{"key":"ref19","article-title":"Veridise","year":"2023"},{"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"},{"key":"ref25","article-title":"The ${\\sf solc}$solc optimizer","year":"2021"},{"key":"ref26","article-title":"Ethereum: A secure decentralised generalised transaction ledger (Berlin version 8fea825\u20132022\u201308-22)","author":"Wood","year":"2022"},{"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"},{"key":"ref35","article-title":"Coq formalisation of the ethereum virtual machine (WIP)","year":"2020"},{"key":"ref36","article-title":"Bedrock Bit Vectors (BBV)","year":"2018"},{"key":"ref37","article-title":"Verification and certification of EVM optimizations","author":"Leal S\u00e1nchez","year":"2024"},{"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"},{"key":"ref39","article-title":"Tightened transitive closure of integer addition constraints","volume-title":"Proc. 8th Symp. Abstraction, Reformulation, Approximation","author":"Revesz"},{"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"},{"key":"ref51","article-title":"Certifying assembly optimizations in Coq by symbolic execution with hash-consing","volume-title":"Proc. Coq Workshop","author":"Gourdin"},{"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":[{"value":"1545-5971","type":"print"},{"value":"1941-0018","type":"electronic"},{"value":"2160-9209","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,7]]}}}