{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T15:52:03Z","timestamp":1778255523912,"version":"3.51.4"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"<jats:p>Callbacks are an effective programming discipline for implementing event-driven programming, especially in environments like Ethereum which forbid shared global state and concurrency. Callbacks allow a callee to delegate the execution back to the caller. Though effective, they can lead to subtle mistakes principally in open environments where callbacks can be added in a new code. Indeed, several high profile bugs in smart contracts exploit callbacks.<\/jats:p>\n          <jats:p>\n            We present the first static technique ensuring\n            <jats:italic>modularity<\/jats:italic>\n            in the presence of callbacks and apply it to verify prominent smart contracts. Modularity ensures that external calls to other contracts cannot affect the behavior of the contract. Importantly, modularity is guaranteed without restricting programming.\n          <\/jats:p>\n          <jats:p>\n            In general, checking modularity is undecidable\u2014even for programs without loops. This paper describes an effective technique for soundly ensuring modularity harnessing SMT solvers. The main idea is to define a constructive version of modularity using\n            <jats:italic>commutativity<\/jats:italic>\n            and\n            <jats:italic>projection<\/jats:italic>\n            operations on program segments. We believe that this approach is also accessible to programmers, since counterexamples to modularity can be generated automatically by the SMT solvers, allowing programmers to understand and fix the error.\n          <\/jats:p>\n          <jats:p>We implemented our approach in order to demonstrate the precision of the modularity analysis and applied it to real smart contracts, including a subset of the 150 most active contracts in Ethereum. Our implementation decompiles bytecode programs into an intermediate representation and then implements the modularity checking using SMT queries. Overall, we argue that our experimental results indicate that the method can be applied to many realistic contracts, and that it is able to prove modularity where other methods fail.<\/jats:p>","DOI":"10.1145\/3428277","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:36:06Z","timestamp":1606260966000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["Taming callbacks for smart contract modularity"],"prefix":"10.1145","volume":"4","author":[{"given":"Elvira","family":"Albert","sequence":"first","affiliation":[{"name":"Complutense University of Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shelly","family":"Grossman","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clara","family":"Rodr\u00edguez-N\u00fa\u00f1ez","sequence":"additional","affiliation":[{"name":"Complutense University of Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Albert","family":"Rubio","sequence":"additional","affiliation":[{"name":"Complutense University of Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_24"},{"key":"e_1_2_2_2_1","unstructured":"Anonymized for the submission. 2020. Anonymized for the submission..  Anonymized for the submission. 2020. Anonymized for the submission.."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54455-6_8"},{"key":"e_1_2_2_4_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Bansal Kshitij","unstructured":"Kshitij Bansal , Eric Koskinen , and Omer Tripp . 2018. Automatic Generation of Precise and Useful Commutativity Conditions . In Tools and Algorithms for the Construction and Analysis of Systems , Dirk Beyer and Marieke Huisman (Eds.). Springer International Publishing , Cham , 115-132. Kshitij Bansal, Eric Koskinen, and Omer Tripp. 2018. Automatic Generation of Precise and Useful Commutativity Conditions. In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer and Marieke Huisman (Eds.). Springer International Publishing, Cham, 115-132."},{"key":"e_1_2_2_5_1","first-page":"170","volume-title":"FMCAD 2019","author":"Barthe Gilles","year":"2019","unstructured":"Gilles Barthe , Renate Eilers , Pamina Georgiou , Bernhard Gleiss , Laura Kov\u00e1cs , and Mateo Mafei . 2019 . Verifying Relational Properties using Trace Logic. In 2019 Formal Methods in Computer Aided Design , FMCAD 2019 , San Jose, CA, USA , October 22-25, 2019. 170 - 178 . Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kov\u00e1cs, and Mateo Mafei. 2019. Verifying Relational Properties using Trace Logic. In 2019 Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22-25, 2019. 170-178."},{"key":"e_1_2_2_6_1","doi-asserted-by":"crossref","unstructured":"Sidi Mohamed Beillahi Gabriela Ciocarlie Michael Emmi and Constantin Enea. 2020. Behavioral Simulation for Smart Contracts. ( 2020 ) To appear.  Sidi Mohamed Beillahi Gabriela Ciocarlie Michael Emmi and Constantin Enea. 2020. Behavioral Simulation for Smart Contracts. ( 2020 ) To appear.","DOI":"10.1145\/3385412.3386022"},{"key":"e_1_2_2_7_1","doi-asserted-by":"crossref","unstructured":"Nick Benton. 2004. Simple relational correctness proofs for static analyses and program transformations. ACM SIGPLAN Notices 39 1 ( 2004 ) 14-25.  Nick Benton. 2004. Simple relational correctness proofs for static analyses and program transformations. ACM SIGPLAN Notices 39 1 ( 2004 ) 14-25.","DOI":"10.1145\/982962.964003"},{"key":"e_1_2_2_8_1","unstructured":"Thomas Bernardi Nurit Dor Anastasia Fedotov Shelly Grossman Alexander Nutz Lior Oppenheim Or Pistiner Mooly Sagiv John Toman and James Wilcox. 2020. Preventing Reentrancy Bugs-Another Use Case for Formal Verification. https:\/\/www.certora.com\/blog\/reentrancy.html.  Thomas Bernardi Nurit Dor Anastasia Fedotov Shelly Grossman Alexander Nutz Lior Oppenheim Or Pistiner Mooly Sagiv John Toman and James Wilcox. 2020. Preventing Reentrancy Bugs-Another Use Case for Formal Verification. https:\/\/www.certora.com\/blog\/reentrancy.html."},{"key":"e_1_2_2_9_1","volume-title":"Concurrency Control and Recovery in Database Systems","author":"Bernstein Philip A.","unstructured":"Philip A. Bernstein , Vassos Hadzilacos , and Nathan Goodman . 1987. Concurrency Control and Recovery in Database Systems . Addison-Wesley . Philip A. Bernstein, Vassos Hadzilacos, and Nathan Goodman. 1987. Concurrency Control and Recovery in Database Systems. Addison-Wesley."},{"key":"e_1_2_2_10_1","unstructured":"Alina Bizga. 2020. A hackers' dream payday: Ledf.Me and Uniswap lose $25 million worth of cryptocurrency. https:\/\/securityboulevard.com\/ 2020 \/04\/a-hackers-dream-payday-ledf-me-and-uniswap-lose-25-million-worthof-cryptocurrency\/. [Online; accessed 11-May-2020].  Alina Bizga. 2020. A hackers' dream payday: Ledf.Me and Uniswap lose $25 million worth of cryptocurrency. https:\/\/securityboulevard.com\/ 2020 \/04\/a-hackers-dream-payday-ledf-me-and-uniswap-lose-25-million-worthof-cryptocurrency\/. [Online; accessed 11-May-2020]."},{"key":"e_1_2_2_11_1","volume-title":"Ethainter: A Smart Contract Security Analyzer for Composite Vulnerabilities. ( 2020 ), To appear.","author":"Brent Lexi","year":"2020","unstructured":"Lexi Brent , Neville Grech , Sifis Lagouvardos , Bernhard Scholz , and Yannis Smaragdakis . 2020 . Ethainter: A Smart Contract Security Analyzer for Composite Vulnerabilities. ( 2020 ), To appear. Lexi Brent, Neville Grech, Sifis Lagouvardos, Bernhard Scholz, and Yannis Smaragdakis. 2020. Ethainter: A Smart Contract Security Analyzer for Composite Vulnerabilities. ( 2020 ), To appear."},{"key":"e_1_2_2_12_1","volume-title":"CRITICAL UPDATE Re: DAO Vulnerability. https:\/\/blog.ethereum.org\/ 2016 \/06\/17\/critical-update-redao-vulnerability\/. [Online","author":"Buterin Vitalik","year":"2017","unstructured":"Vitalik Buterin . 2016. CRITICAL UPDATE Re: DAO Vulnerability. https:\/\/blog.ethereum.org\/ 2016 \/06\/17\/critical-update-redao-vulnerability\/. [Online ; accessed 2- July - 2017 ]. Vitalik Buterin. 2016. CRITICAL UPDATE Re: DAO Vulnerability. https:\/\/blog.ethereum.org\/ 2016 \/06\/17\/critical-update-redao-vulnerability\/. [Online; accessed 2-July-2017]."},{"key":"e_1_2_2_13_1","volume-title":"Securing Smart Contracts with Information Flow. In Third International Symposium on Foundations and Applications of Blockchain","author":"Ceccheti Ethan","year":"2020","unstructured":"Ethan Ceccheti , Siqiu Yao , Haobin Ni , and Andrew Myers . 2020 . Securing Smart Contracts with Information Flow. In Third International Symposium on Foundations and Applications of Blockchain 2020. Ethan Ceccheti, Siqiu Yao, Haobin Ni, and Andrew Myers. 2020. Securing Smart Contracts with Information Flow. In Third International Symposium on Foundations and Applications of Blockchain 2020."},{"key":"e_1_2_2_14_1","volume-title":"Ethereum Smart Contract Best Practices. https:\/\/consensys.github.io\/smart-contract-best-practices\/ known_attacks\/. [Online","year":"2020","unstructured":"Consensys. 2019. Ethereum Smart Contract Best Practices. https:\/\/consensys.github.io\/smart-contract-best-practices\/ known_attacks\/. [Online ; accessed 14- May - 2020 ]. Consensys. 2019. Ethereum Smart Contract Best Practices. https:\/\/consensys.github.io\/smart-contract-best-practices\/ known_attacks\/. [Online; accessed 14-May-2020]."},{"key":"e_1_2_2_15_1","unstructured":"Phil Daian. 2016. ( 2016 ). http:\/\/hackingdistributed.com\/ 2016 \/06\/18\/ analysis-of-the-dao-exploit\/  Phil Daian. 2016. ( 2016 ). http:\/\/hackingdistributed.com\/ 2016 \/06\/18\/ analysis-of-the-dao-exploit\/"},{"key":"e_1_2_2_16_1","first-page":"337","volume-title":"Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest, Hungary) ( TACAS'08\/ETAPS'08)","author":"Moura Leonardo De","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner . [n.d.]. Z3 : An Eficient SMT Solver . In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest, Hungary) ( TACAS'08\/ETAPS'08) . Springer-Verlag, Berlin, Heidelberg , 337 - 340 . Leonardo De Moura and Nikolaj Bj\u00f8rner. [n.d.]. Z3: An Eficient SMT Solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest, Hungary) ( TACAS'08\/ETAPS'08). Springer-Verlag, Berlin, Heidelberg, 337-340."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/WETSEB.2019.00008"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363263"},{"key":"e_1_2_2_19_1","doi-asserted-by":"crossref","unstructured":"Bernd Finkbeiner Christopher Hahn Marvin Stenger and Leander Tentrup. 2019. Monitoring hyperproperties. Formal Methods Syst. Des. 54 3 ( 2019 ) 336-363.  Bernd Finkbeiner Christopher Hahn Marvin Stenger and Leander Tentrup. 2019. Monitoring hyperproperties. Formal Methods Syst. Des. 54 3 ( 2019 ) 336-363.","DOI":"10.1007\/s10703-019-00334-z"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781169"},{"key":"e_1_2_2_21_1","volume-title":"Foundations and Tools for the Static Analysis of Ethereum Smart Contracts","author":"Grishchenko Ilya","unstructured":"Ilya Grishchenko , Mateo Mafei , and Clara Schneidewind . 2018a. Foundations and Tools for the Static Analysis of Ethereum Smart Contracts . In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing , Cham , 51-78. Ilya Grishchenko, Mateo Mafei, and Clara Schneidewind. 2018a. Foundations and Tools for the Static Analysis of Ethereum Smart Contracts. In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing, Cham, 51-78."},{"key":"e_1_2_2_22_1","volume-title":"Principles of Security and Trust, Lujo Bauer and Ralf K\u00fcsters (Eds.)","author":"Grishchenko Ilya","unstructured":"Ilya Grishchenko , Mateo Mafei , and Clara Schneidewind . 2018b. A Semantic Framework for the Security Analysis of Ethereum Smart Contracts . In Principles of Security and Trust, Lujo Bauer and Ralf K\u00fcsters (Eds.) . Springer International Publishing , Cham , 243-269. Ilya Grishchenko, Mateo Mafei, and Clara Schneidewind. 2018b. A Semantic Framework for the Security Analysis of Ethereum Smart Contracts. In Principles of Security and Trust, Lujo Bauer and Ralf K\u00fcsters (Eds.). Springer International Publishing, Cham, 243-269."},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Shelly Grossman Itai Abraham Guy Golan-Gueta Yan Michalevsky Noam Rinetzky Mooly Sagiv and Yoni Zohar. 2018. Online detection of efectively callback free objects with applications to smart contracts. PACMPL 2 POPL ( 2018 ) 48 : 1-48 : 28.  Shelly Grossman Itai Abraham Guy Golan-Gueta Yan Michalevsky Noam Rinetzky Mooly Sagiv and Yoni Zohar. 2018. Online detection of efectively callback free objects with applications to smart contracts. PACMPL 2 POPL ( 2018 ) 48 : 1-48 : 28.","DOI":"10.1145\/3158136"},{"key":"e_1_2_2_24_1","volume-title":"Understanding Callbacks and Promises. https:\/\/dev.to\/_ferh97\/ understanding-callbacks-andpromises-3fd5. [Online","author":"Hernandez Fernando","year":"2020","unstructured":"Fernando Hernandez . 2019. Understanding Callbacks and Promises. https:\/\/dev.to\/_ferh97\/ understanding-callbacks-andpromises-3fd5. [Online ; accessed 14- May - 2020 ]. Fernando Hernandez. 2019. Understanding Callbacks and Promises. https:\/\/dev.to\/_ferh97\/ understanding-callbacks-andpromises-3fd5. [Online; accessed 14-May-2020]."},{"key":"e_1_2_2_25_1","volume-title":"Security Alert: Ethereum Constantinople Postponement. https:\/\/blog.ethereum.org\/ 2019 \/01\/15\/ security-alert-ethereum-constantinople-postponement\/. [Online","author":"Jameson Hudson","year":"2019","unstructured":"Hudson Jameson . 2019 . Security Alert: Ethereum Constantinople Postponement. https:\/\/blog.ethereum.org\/ 2019 \/01\/15\/ security-alert-ethereum-constantinople-postponement\/. [Online ; accessed 11-May-2020]. Hudson Jameson. 2019. Security Alert: Ethereum Constantinople Postponement. https:\/\/blog.ethereum.org\/ 2019 \/01\/15\/ security-alert-ethereum-constantinople-postponement\/. [Online; accessed 11-May-2020]."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330560"},{"key":"e_1_2_2_27_1","unstructured":"Patrick Lam Eric Bodden Ondrej Lhot\u00e1k and Laurie Hendren. 2011. The Soot framework for Java program analysis: a retrospective.  Patrick Lam Eric Bodden Ondrej Lhot\u00e1k and Laurie Hendren. 2011. The Soot framework for Java program analysis: a retrospective."},{"key":"e_1_2_2_28_1","volume-title":"Jemin Andrew Choi, and Fan Long","author":"Li Ao","year":"2020","unstructured":"Ao Li , Jemin Andrew Choi, and Fan Long . 2020 . Securing Smart Contract with Runtime Validation. ( 2020 ), To appear. Ao Li, Jemin Andrew Choi, and Fan Long. 2020. Securing Smart Contract with Runtime Validation. ( 2020 ), To appear."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_2_2_31_1","volume-title":"Tool Demonstration: FSolidM for Designing Secure Ethereum Smart Contracts. In Principles of Security and Trust, Lujo Bauer and Ralf K\u00fcsters (Eds.)","author":"Mavridou Anastasia","year":"2018","unstructured":"Anastasia Mavridou and Aron Laszka . 2018 . Tool Demonstration: FSolidM for Designing Secure Ethereum Smart Contracts. In Principles of Security and Trust, Lujo Bauer and Ralf K\u00fcsters (Eds.) . Springer International Publishing , Cham , 270-277. Anastasia Mavridou and Aron Laszka. 2018. Tool Demonstration: FSolidM for Designing Secure Ethereum Smart Contracts. In Principles of Security and Trust, Lujo Bauer and Ralf K\u00fcsters (Eds.). Springer International Publishing, Cham, 270-277."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274743"},{"key":"e_1_2_2_33_1","volume-title":"https:\/\/www.coindesk.com\/spankchainloses-40k-in-hack-due-to-smart-contract-bug. [Online","author":"Palmer Daniel","year":"2020","unstructured":"Daniel Palmer . 2018. SpankChain Loses $40K in Hack Due to Smart Contract Bug . https:\/\/www.coindesk.com\/spankchainloses-40k-in-hack-due-to-smart-contract-bug. [Online ; accessed 11- May - 2020 ]. Daniel Palmer. 2018. SpankChain Loses $40K in Hack Due to Smart Contract Bug. https:\/\/www.coindesk.com\/spankchainloses-40k-in-hack-due-to-smart-contract-bug. [Online; accessed 11-May-2020]."},{"key":"e_1_2_2_34_1","volume-title":"Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Atacks. In 26th Annual Network and Distributed System Security Symposium, NDSS 2019","author":"Rodler Michael","year":"2019","unstructured":"Michael Rodler , Wenting Li , Ghassan O. Karame , and Lucas Davi . 2019 . Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Atacks. In 26th Annual Network and Distributed System Security Symposium, NDSS 2019 , San Diego, California, USA , February 24-27, 2019. The Internet Society. https:\/\/www.ndss-symposium.org\/ndss-paper\/sereumprotecting-existing-smart-contracts-against-re-entrancy-attacks\/ Michael Rodler, Wenting Li, Ghassan O. Karame, and Lucas Davi. 2019. Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Atacks. In 26th Annual Network and Distributed System Security Symposium, NDSS 2019, San Diego, California, USA, February 24-27, 2019. The Internet Society. https:\/\/www.ndss-symposium.org\/ndss-paper\/sereumprotecting-existing-smart-contracts-against-re-entrancy-attacks\/"},{"key":"e_1_2_2_35_1","doi-asserted-by":"crossref","unstructured":"Clara Schneidewind Markus Scherer Ilya Grishchenko and Mateo Mafei. 2020. eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. ( 2020 ) To appear.  Clara Schneidewind Markus Scherer Ilya Grishchenko and Mateo Mafei. 2020. eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. ( 2020 ) To appear.","DOI":"10.1145\/3372297.3417250"},{"key":"e_1_2_2_36_1","volume-title":"A Concurrent Perspective on Smart Contracts","author":"Sergey Ilya","unstructured":"Ilya Sergey and Aquinas Hobor . 2017. A Concurrent Perspective on Smart Contracts . In Financial Cryptography and Data Security, Michael Brenner, Kurt Rohlof, Joseph Bonneau, Andrew Miller, Peter Y.A. Ryan, Vanessa Teague, Andrea Bracciali, Massimiliano Sala, Federico Pintore, and Markus Jakobsson (Eds.). Springer International Publishing , Cham , 478-493. Ilya Sergey and Aquinas Hobor. 2017. A Concurrent Perspective on Smart Contracts. In Financial Cryptography and Data Security, Michael Brenner, Kurt Rohlof, Joseph Bonneau, Andrew Miller, Peter Y.A. Ryan, Vanessa Teague, Andrea Bracciali, Massimiliano Sala, Federico Pintore, and Markus Jakobsson (Eds.). Springer International Publishing, Cham, 478-493."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_2_2_38_1","unstructured":"Synthetix. 2020. Synthetix-Decentralised synthetic assets. www.synthetix.io.  Synthetix. 2020. Synthetix-Decentralised synthetic assets. www.synthetix.io."},{"key":"e_1_2_2_39_1","volume-title":"https:\/\/defipulse.com\/. [Online","author":"Open Community The Concourse","year":"2020","unstructured":"The Concourse Open Community . 2019. DeFi Pulse . https:\/\/defipulse.com\/. [Online ; accessed 11- May - 2020 ]. The Concourse Open Community. 2019. DeFi Pulse. https:\/\/defipulse.com\/. [Online; accessed 11-May-2020]."},{"key":"e_1_2_2_40_1","volume-title":"SmartCheck: Static Analysis of Ethereum Smart Contracts. In 2018 IEEE\/ACM 1st International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB). 9-16","author":"Tikhomirov S.","unstructured":"S. Tikhomirov , E. Voskresenskaya , I. Ivanitskiy , R. Takhaviev , E. Marchenko , and Y. Alexandrov . 2018 . SmartCheck: Static Analysis of Ethereum Smart Contracts. In 2018 IEEE\/ACM 1st International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB). 9-16 . S. Tikhomirov, E. Voskresenskaya, I. Ivanitskiy, R. Takhaviev, E. Marchenko, and Y. Alexandrov. 2018. SmartCheck: Static Analysis of Ethereum Smart Contracts. In 2018 IEEE\/ACM 1st International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB). 9-16."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254083"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243780"},{"key":"e_1_2_2_43_1","volume-title":"imBTC Uniswap Pool Drained for $300k in ETH. https:\/\/defirate.com\/imbtc-uniswap-hack\/. [Online","author":"Turley Cooper","year":"2020","unstructured":"Cooper Turley . 2020. imBTC Uniswap Pool Drained for $300k in ETH. https:\/\/defirate.com\/imbtc-uniswap-hack\/. [Online ; accessed 11- May - 2020 ]. Cooper Turley. 2020. imBTC Uniswap Pool Drained for $300k in ETH. https:\/\/defirate.com\/imbtc-uniswap-hack\/. [Online; accessed 11-May-2020]."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_29"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065944.1065953"},{"key":"e_1_2_2_46_1","volume-title":"Formal Specification and Verification of Smart Contracts for Azure Blockchain., 13 pages. arXiv","author":"Want Yuepeng","year":"1812","unstructured":"Yuepeng Want , Shuvendu Lahiri , Shuo Chen , Rong Pan , Isil Dillig , Cody Bprb , and Immad Naseer . 2019. Formal Specification and Verification of Smart Contracts for Azure Blockchain., 13 pages. arXiv : 1812 .08829v2. Yuepeng Want, Shuvendu Lahiri, Shuo Chen, Rong Pan, Isil Dillig, Cody Bprb, and Immad Naseer. 2019. Formal Specification and Verification of Smart Contracts for Azure Blockchain., 13 pages. arXiv: 1812.08829v2."},{"key":"e_1_2_2_47_1","volume-title":"Ethereum: A Secure Decentralised Generalised Transaction Ledger","author":"Wood Gavin","year":"2016","unstructured":"Gavin Wood . 2016 . Ethereum: A Secure Decentralised Generalised Transaction Ledger . http:\/\/gavwood.com\/paper.pdf. [Online; accessed 5-July-2017]. Gavin Wood. 2016. Ethereum: A Secure Decentralised Generalised Transaction Ledger. http:\/\/gavwood.com\/paper.pdf. [Online; accessed 5-July-2017]."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428277","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428277","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:57Z","timestamp":1750197777000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428277"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":47,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428277"],"URL":"https:\/\/doi.org\/10.1145\/3428277","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}