{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:32:34Z","timestamp":1770283954042,"version":"3.49.0"},"reference-count":86,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100013209","name":"Hellenic Foundation for Research and Innovation","doi-asserted-by":"publisher","award":["4127"],"award-info":[{"award-number":["4127"]}],"id":[{"id":"10.13039\/501100013209","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,10,20]]},"abstract":"<jats:p>We present a static analysis approach that combines concrete values and symbolic expressions. This symbolic value-flow (\u201csymvalic\u201d) analysis models program behavior with high precision, e.g., full path sensitivity. To achieve deep modeling of program semantics, the analysis relies on a symbiotic relationship between a traditional static analysis fixpoint computation and a symbolic solver: the solver does not merely receive a complex \u201cpath condition\u201d to solve, but is instead invoked repeatedly (often tens or hundreds of thousands of times), in close cooperation with the flow computation of the analysis.<\/jats:p>\n          <jats:p>The result of the symvalic analysis architecture is a static modeling of program behavior that is much more complete than symbolic execution, much more precise than conventional static analysis, and domain-agnostic: no special-purpose definition of anti-patterns is necessary in order to compute violations of safety conditions with high precision.<\/jats:p>\n          <jats:p>We apply the analysis to the domain of Ethereum smart contracts. This domain represents a fundamental challenge for program analysis approaches: despite numerous publications, research work has not been effective at uncovering vulnerabilities of high real-world value.<\/jats:p>\n          <jats:p>In systematic comparison of symvalic analysis with past tools, we find significantly increased completeness (shown as 83-96% statement coverage and more true error reports) combined with much higher precision, as measured by rate of true positive reports. In terms of real-world impact, since the beginning of 2021, the analysis has resulted in the discovery and disclosure of several critical vulnerabilities, over funds in the many millions of dollars. Six separate bug bounties totaling over $350K have been awarded for these disclosures.<\/jats:p>","DOI":"10.1145\/3485540","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Symbolic value-flow static analysis: deep, precise, complete modeling of Ethereum smart contracts"],"prefix":"10.1145","volume":"5","author":[{"given":"Yannis","family":"Smaragdakis","sequence":"first","affiliation":[{"name":"University of Athens, Greece"}]},{"given":"Neville","family":"Grech","sequence":"additional","affiliation":[{"name":"University of Malta, Malta"}]},{"given":"Sifis","family":"Lagouvardos","sequence":"additional","affiliation":[{"name":"University of Athens, Greece"}]},{"given":"Konstantinos","family":"Triantafyllou","sequence":"additional","affiliation":[{"name":"University of Athens, Greece"}]},{"given":"Ilias","family":"Tsatiris","sequence":"additional","affiliation":[{"name":"University of Athens, Greece"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151649"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_7"},{"key":"e_1_2_2_3_1","volume-title":"Automated Technology for Verification and Analysis (ATVA)","author":"Albert Elvira"},{"key":"e_1_2_2_4_1","volume-title":"Schett","author":"Albert Elvira","year":"2020"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428277"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792771"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428209"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2491976"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978428"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385990"},{"key":"e_1_2_2_12_1","volume-title":"Vandal: A Scalable Security Analysis Framework for Smart Contracts. CoRR, abs\/1802.08660","author":"Brent Lexi","year":"2018"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855741.1855756"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TETC.2020.2979019"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1961296.1950396"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3474085.3475399"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_2_2_19_1","volume-title":"Software Engineering","author":"Czech Mike","year":"2016"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_2_21_1","unstructured":"Dedaub. 2021. Ethereum Pawn Stars: \u2019$5.7M in hard assets? Best I can do is $2.3M\u2019. https:\/\/medium.com\/dedaub\/ethereum-pawn-stars-5-7m-in-hard-assets-best-i-can-do-is-2-3m-b93604be503e  Dedaub. 2021. Ethereum Pawn Stars: \u2019$5.7M in hard assets? Best I can do is $2.3M\u2019. https:\/\/medium.com\/dedaub\/ethereum-pawn-stars-5-7m-in-hard-assets-best-i-can-do-is-2-3m-b93604be503e"},{"key":"e_1_2_2_22_1","unstructured":"Dedaub. 2021. Killing a Bad (Arbitrage) Bot ... to Save its Owners. https:\/\/medium.com\/dedaub\/killing-a-bad-arbitrage-bot-f29e7e808c7d  Dedaub. 2021. Killing a Bad (Arbitrage) Bot ... to Save its Owners. https:\/\/medium.com\/dedaub\/killing-a-bad-arbitrage-bot-f29e7e808c7d"},{"key":"e_1_2_2_23_1","unstructured":"Dedaub. 2021. Look Ma\u2019 no source! Hacking a DeFi Service with No Source Code Available. https:\/\/medium.com\/dedaub\/look-ma-no-source-hacking-a-defi-service-with-no-source-code-available-c40a6583f28f  Dedaub. 2021. Look Ma\u2019 no source! Hacking a DeFi Service with No Source Code Available. https:\/\/medium.com\/dedaub\/look-ma-no-source-hacking-a-defi-service-with-no-source-code-available-c40a6583f28f"},{"key":"e_1_2_2_24_1","volume-title":"Yield Skimming: Forcing Bad Swaps on Yield Farming. https:\/\/medium.com\/dedaub\/yield-skimming-forcing-bad-swaps-on-yield-farming-397361fd7c72?source=friends_link&sk=d146b3640321f0a3ccc80540b54368ff","year":"2021"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1134\/S0361768817050024"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380364"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/3235924.3235954"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/WETSEB.2019.00008"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040315"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190226"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_2_32_1","first-page":"151","article-title":"Automated Whitebox Fuzz Testing","volume":"8","author":"Godefroid Patrice","year":"2008","journal-title":"NDSS."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2090147.2094081"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00120"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276486"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3404366"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158136"},{"key":"e_1_2_2_38_1","volume-title":"solc-verify: A Modular Verifier for Solidity Smart Contracts","author":"Hajdu \u00c1kos"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363230"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00022"},{"key":"e_1_2_2_41_1","unstructured":"J.J. Honig. 2020. Incremental symbolic execution. http:\/\/essay.utwente.nl\/81526\/  J.J. Honig. 2020. Incremental symbolic execution. http:\/\/essay.utwente.nl\/81526\/"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592438"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238177"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_2_45_1","volume-title":"Weakly Sensitive Analysis for Unbounded Iteration over JavaScript Objects","author":"Ko Yoonseok"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330560"},{"key":"e_1_2_2_47_1","volume-title":"July 15, 2021]. ETHSecurity Community Telegram channel.","author":"Konstantopoulos Georgios","year":"2021"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/3277203.3277303"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428258"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509553"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2008.306"},{"key":"e_1_2_2_53_1","unstructured":"Michales Jonah. 2021. Inside the War Room That Saved Primitive Finance. https:\/\/medium.com\/immunefi\/inside-the-war-room-that-saved-primitive-finance-6509e2188c86  Michales Jonah. 2021. Inside the War Room That Saved Primitive Finance. https:\/\/medium.com\/immunefi\/inside-the-war-room-that-saved-primitive-finance-6509e2188c86"},{"key":"e_1_2_2_54_1","volume-title":"Schwartzbach","author":"M\u00f8ller Anders","year":"2018"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00133"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380334"},{"key":"e_1_2_2_57_1","volume-title":"Proc. 34th European Conference on Object-Oriented Programming (ECOOP).","author":"Nielsen Benjamin Barslev","year":"2020"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.5555\/555142"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274743"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.5555\/648251.752211"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487568.2487569"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393636"},{"key":"e_1_2_2_63_1","volume-title":"Smart Contract Vulnerabilities: Vulnerable Does Not Imply Exploited. In 30th USENIX Security Symposium (USENIX Security 21)","author":"Perez Daniel","year":"2021"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00024"},{"key":"e_1_2_2_65_1","unstructured":"Primitive Finance. 2021. PrimitiveFi post-mortem analysis. https:\/\/primitivefinance.medium.com\/postmortem-on-the-primitive-finance-whitehack-of-february-21st-2021-17446c0f3122  Primitive Finance. 2021. PrimitiveFi post-mortem analysis. https:\/\/primitivefinance.medium.com\/postmortem-on-the-primitive-finance-whitehack-of-february-21st-2021-17446c0f3122"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275501"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372297.3417250"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_38"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095430.1081750"},{"key":"e_1_2_2_70_1","volume-title":"Program flow analysis: theory and applications, Steven S","author":"Sharir Micha"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5494813"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360566"},{"key":"e_1_2_2_73_1","unstructured":"The Certora team. 2017. The Certora Prover. https:\/\/www.certora.com  The Certora team. 2017. The Certora Prover. https:\/\/www.certora.com"},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3194113.3194115"},{"key":"e_1_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792786.1792798"},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2006.117"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274737"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.5555\/3361338.3361449"},{"key":"e_1_2_2_79_1","unstructured":"Trail of Bits. 2020. Trail of Bits comments on average coverage. https:\/\/forum.openzeppelin.com\/t\/symbolic-execution\/2158\/3 Accessed: 2020-11-20.  Trail of Bits. 2020. Trail of Bits comments on average coverage. https:\/\/forum.openzeppelin.com\/t\/symbolic-execution\/2158\/3 Accessed: 2020-11-20."},{"key":"e_1_2_2_80_1","unstructured":"Trail of Bits. 2020. Tweet on symbolic execution coverage. https:\/\/twitter.com\/trailofbits\/status\/1223386823084384256 Accessed: 2020-11-20.  Trail of Bits. 2020. Tweet on symbolic execution coverage. https:\/\/twitter.com\/trailofbits\/status\/1223386823084384256 Accessed: 2020-11-20."},{"key":"e_1_2_2_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243780"},{"key":"e_1_2_2_82_1","unstructured":"Various. 2017. libFuzzer \u2013 a library for coverage-guided fuzz testing. https:\/\/llvm.org\/docs\/LibFuzzer.html  Various. 2017. libFuzzer \u2013 a library for coverage-guided fuzz testing. https:\/\/llvm.org\/docs\/LibFuzzer.html"},{"key":"e_1_2_2_83_1","unstructured":"Various. 2020. SmartBugs: A Framework to Analyze Solidity Smart Contracts. https:\/\/github.com\/smartbugs\/smartbugs  Various. 2020. SmartBugs: A Framework to Analyze Solidity Smart Contracts. https:\/\/github.com\/smartbugs\/smartbugs"},{"key":"e_1_2_2_84_1","volume-title":"Ethereum: A secure decentralised generalised transaction ledger","author":"Wood Gavin","year":"2014"},{"key":"e_1_2_2_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3417064"},{"key":"e_1_2_2_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380388"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485540","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485540","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:40Z","timestamp":1750191520000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485540"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":86,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485540"],"URL":"https:\/\/doi.org\/10.1145\/3485540","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}