{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,7]],"date-time":"2026-08-07T07:56:52Z","timestamp":1786089412809,"version":"3.56.0"},"reference-count":261,"publisher":"Emerald","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,6,30]]},"abstract":"<jats:p>Blockchains have become an integrated part of our finance infrastructures. Being monetary yet fully automated, blockchains and their applications are unanimously deemed impracticable before undergoing necessary verification. This monograph reviews the previous attempts at verifying two fundamental properties of blockchains: correctness (where flaws lead to unintentional damages) and security (where vulnerabilities incur attacks and losses). First, it summarizes and categorizes the correctness and security flaws encountered by real-world blockchains. Second, it systematizes the development of formal verification to address the flaws in blockchains, covering the aspects of models, specifications, and techniques. Third, it unveils the progress of security analysis for mitigating the flaws, unveiling the analysis principles being followed, the flaw oracles being devised, and the detection methods being used. Finally, it summarizes the challenges remaining to be addressed, followed by our vision of the trend in the near future. Throughout this monograph, we anticipate shedding light on future blockchain verification advances, especially in expanding its applicability, making specification generation easier, and discovering previously unknown vulnerabilities. By identifying gaps such as missing tools for infrastructure-level components and the difficulty of writing formal specifications, this work aims to motivate the development of more automated, intelligent, and practical verification frameworks.<\/jats:p>","DOI":"10.1561\/3300000044","type":"journal-article","created":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T09:38:32Z","timestamp":1749029912000},"page":"1-121","source":"Crossref","is-referenced-by-count":4,"title":["Security Analysis and Formal Verification on Blockchain and its Applications"],"prefix":"10.1108","volume":"8","author":[{"given":"Kang","family":"Li","sequence":"first","affiliation":[{"name":"CertiK ,","place":["USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ronghui","family":"Gu","sequence":"additional","affiliation":[{"name":"Columbia University ,","place":["USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jun","family":"Xu","sequence":"additional","affiliation":[{"name":"The University of Utah ,","place":["USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhaofeng","family":"Chen","sequence":"additional","affiliation":[{"name":"CertiK ,","place":["USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Siwei","family":"Wu","sequence":"additional","affiliation":[{"name":"Zhejiang University ,","place":["China"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yajin","family":"Zhou","sequence":"additional","affiliation":[{"name":"Zhejiang University ,","place":["China"]},{"name":"BlockSec ,","place":["Hong Kong"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mu","family":"Zhang","sequence":"additional","affiliation":[{"name":"The University of Utah ,","place":["USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xiapu","family":"Luo","sequence":"additional","affiliation":[{"name":"The Hong Kong Polytechnic University ,","place":["Hong Kong"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yuzhe","family":"Tang","sequence":"additional","affiliation":[{"name":"Syracuse University ,","place":["USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yi","family":"Li","sequence":"additional","affiliation":[{"name":"Nanyang Technological University ,","place":["Singapore"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xiaokuan","family":"Zhang","sequence":"additional","affiliation":[{"name":"George Mason University ,","place":["USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yibo","family":"Wang","sequence":"additional","affiliation":[{"name":"Syracuse University ,","place":["USA"]}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"140","published-online":{"date-parts":[[2025,6,30]]},"reference":[{"key":"2026033014314832300_ref001","doi-asserted-by":"crossref","first-page":"270","DOI":"10.1007\/978-3-319-96145-3_15","volume-title":"International Conference on Computer Aided Verification","author":"Abate","year":"2018"},{"key":"2026033014314832300_ref002","first-page":"1775","article-title":"Smart learning to find dumb contracts","author":"Abdelaziz","year":"2023","journal-title":"32nd USENIX Security Symposium (USENIX Security 23)"},{"key":"2026033014314832300_ref003","unstructured":"Alchemy\n          . (2022). \u201cHow to Send Private Transactions on Ethereum\u201d. url:  https:\/\/www.alchemy.com\/overviews\/ethereum-private-transactions."},{"key":"2026033014314832300_ref004","unstructured":"Aleth\n          . (2021). \u201cEthereum C++ client, tools and libraries\u201d. url: https:\/\/github.com\/ethereum\/aleth."},{"key":"2026033014314832300_ref005","doi-asserted-by":"crossref","first-page":"101227","DOI":"10.1016\/j.pmcj.2020.101227","article-title":"Verification of smart contracts: A survey","volume":"67","author":"Almakhour","year":"2020","journal-title":"Pervasive and Mobile Computing"},{"key":"2026033014314832300_ref006","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-031-13185-1\\_16","volume-title":"Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I","author":"Alt","year":"2022"},{"key":"2026033014314832300_ref007","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1007\/978-3-030-54994-7_27","volume-title":"Formal Methods. FM 2019 International Workshops: Porto, Portugal, October 7\u201311, 2019, Revised Selected Papers, Part I 3","author":"Alturki","year":"2020"},{"key":"2026033014314832300_ref008","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1007\/3-540-48683-6_3","volume-title":"Computer Aided Verification: 11th International Conference, CAV\u201999 Trento, Italy, July 6\u201310, 1999 Proceedings 11","author":"Alur","year":"1999"},{"key":"2026033014314832300_ref009","unstructured":"Analog\n            \n          . (2022). \u201cA Timeline and History of Recent Cross-Chain Bridge Attacks\u201d. url: https:\/\/medium.com\/@analogtime\/a-timeline-and-history-of-recent-cross-chain-bridge-attacks-analog-insights-507349381a4b."},{"key":"2026033014314832300_ref010","doi-asserted-by":"publisher","first-page":"99552","DOI":"10.1109\/ACCESS.2020.2995183","article-title":"GasFuzzer: Fuzzing Ethereum Smart Contract Binaries to Expose Gas-Oriented Exception Security Vulnerabilities","volume":"8","author":"Ashraf","year":"2020","journal-title":"IEEE Access"},{"key":"2026033014314832300_ref011","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/978-3-662-54455-6_8","volume-title":"Principles of Security and Trust: 6th International Conference, POST 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings 6","author":"Atzei","year":"2017"},{"issue":"3","key":"2026033014314832300_ref012","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3182657","article-title":"A survey of symbolic execution techniques","volume":"51","author":"Baldoni","year":"2018","journal-title":"ACM Computing Surveys (CSUR)"},{"issue":"3","key":"2026033014314832300_ref013","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1109\/MS.2011.27","article-title":"Rigorous component-based system design using the BIP framework","volume":"28","author":"Basu","year":"2011","journal-title":"IEEE software"},{"issue":"2","key":"2026033014314832300_ref014","doi-asserted-by":"publisher","first-page":"1132","DOI":"10.1109\/TR.2023.3336246","article-title":"Hephaestus: Modeling, Analysis, and Performance Evaluation of Cross-Chain Transactions","volume":"73","author":"Belchior","year":"2024","journal-title":"IEEE Trans. Reliab"},{"key":"2026033014314832300_ref015","article-title":"Reusable Formal Verification of DAG-based Consensus Protocols","author":"Bertrand","year":"2024","journal-title":"arXiv preprint arXiv:2407.02167"},{"key":"2026033014314832300_ref016","article-title":"Holistic verification of blockchain consensus","author":"Bertrand","year":"2022","journal-title":"arXiv preprint arXiv:2206.04489"},{"key":"2026033014314832300_ref017","unstructured":"Blanchard, J. and A.Popowycz. (2023). \u201cAnalysis & Remediation of the Precompile Attack on the Hedera Network\u201d. url:https:\/\/hedera.com\/blog\/analysis-remediation-of-the-precompile-attack-on-the-hedera-network."},{"key":"2026033014314832300_ref018","unstructured":"Block, T.\n           (2023). \u201cBlockSec prevents $5 million from being stolen on Paraspace\u201d. url: https:\/\/www.theblock.co\/post\/220761\/blocksec-prevents-5-million-from-being-stolen-on-paraspace."},{"key":"2026033014314832300_ref019","unstructured":"BlockSec\n          . (2021a). \u201cA Short Analysis of the Wild Exploitation of CVE-2021\u201339137\u201d. url:https:\/\/blocksec.com\/blog\/a-short-analysis-of-the-wild-exploitation-of-cve-2021-39137."},{"key":"2026033014314832300_ref020","unstructured":"BlockSec\n            \n          . (2021b). \u201cNew Integer Overflow Bug Discovered in Solana rBPF\u201d. url:https:\/\/blocksec.com\/blog\/new-integer-overflow-bug-discovered-in-solana-r-bpf."},{"key":"2026033014314832300_ref021","unstructured":"BlockSec\n            \n          . (2023a). \u201c#10: ThirdWeb Incident: Incompatibility Between Trusted Modules Exposes Vulnerability\u201d. url:https:\/\/blocksec.com\/blog\/10-third-web-incident-incompatibility-between-trusted-modules-exposes-vulnerability."},{"key":"2026033014314832300_ref022","unstructured":"BlockSec\n            \n          . (2023b). \u201cSystematic Approach to Maintaining EVM Compatibility and Security\u201d. url:https:\/\/blocksecteam.medium.com\/systematic-approach-to-maintaining-evm-compatibility-and-security-32d0f42846f5."},{"key":"2026033014314832300_ref023","unstructured":"BlockSec\n            \n          . (2024a). \u201cReflecting on Reflection Tokens: A Security Perspective\u201d. url:blocksec.com\/blog\/reflecting-on-reflection-tokens-a-security-perspective."},{"key":"2026033014314832300_ref024","unstructured":"BlockSec\n          . (2024b). \u201cSecurity Check: Do EVM-Compatible Chains Hold Up?\u201d url: https:\/\/blocksec.com\/blog\/security-check-do-evm-compatible-chains-hold-up."},{"key":"2026033014314832300_ref025","first-page":"1829","article-title":"Proxy hunting:understanding and characterizing proxy-based upgradeable smart contracts in blockchains","author":"Bodell","year":"2023","journal-title":"32nd USENIX Security Symposium (USENIX Security 23)"},{"key":"2026033014314832300_ref026","first-page":"46","article-title":"Static taint analysis tools to detect information flows","author":"Boxler","year":"2018","journal-title":"Proceedings of the International Conference on Software Engineering Research and Practice (SERP)"},{"key":"2026033014314832300_ref027","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"International Workshop on Verification, Model Checking, and Abstract Interpretation","author":"Bradley","year":"2011"},{"key":"2026033014314832300_ref028","doi-asserted-by":"crossref","first-page":"454","DOI":"10.1145\/3385412.3385990","article-title":"Ethainter: a smart contract security analyzer for composite vulnerabilities","author":"Brent","year":"2020","journal-title":"Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation"},{"key":"2026033014314832300_ref029","article-title":"Vandal: A scalable security analysis framework for smart contracts","author":"Brent","year":"2018","journal-title":"arXiv preprint arXiv:1809.03981"},{"key":"2026033014314832300_ref030","first-page":"1","article-title":"Symposium on decision problems: On a decision method in restricted second order arithmetic","author":"B\u00fcchi","year":"1966","journal-title":"Studies in Logic and the Foundations of Mathematics"},{"key":"2026033014314832300_ref031","volume-title":"PhD thesis","author":"Buchman","year":"2016"},{"key":"2026033014314832300_ref032","volume-title":"P2P networking and applications","author":"Buford","year":"2009"},{"key":"2026033014314832300_ref033","first-page":"22","article-title":"Ethereum white paper","volume":"1","author":"Buterin","year":"2013","journal-title":"GitHub repository"},{"key":"2026033014314832300_ref034","unstructured":"Caversaccio, P.\n           (2024). \u201cpcaversaccio\/reentrancy-attacks: A chronological and (hopefully) complete list of reentrancy attacks to date.\u201d url:https:\/\/github.com\/pcaversaccio\/reentrancy-attacks."},{"key":"2026033014314832300_ref035","doi-asserted-by":"crossref","first-page":"1249","DOI":"10.1109\/SP40001.2021.00084","volume-title":"2021 IEEE Symposium on Security and Privacy (SP)","author":"Cecchetti","year":"2021"},{"key":"2026033014314832300_ref036","unstructured":"CertiK\n            \n          . (2023). \u201cThe HamsterWheel: An In-Depth Exploration of a Novel Attack Vector on the Sui Blockchain\u201d. url: https:\/\/www.certik.com\/resources\/blog\/the-hamsterwheel-an-in-depth-exploration-of-a-novel-attack-vector-on-the-sui."},{"key":"2026033014314832300_ref037","unstructured":"Chain-Split, B. C.\n           (2018). \u201cBitcoin Cash Chain-Split Bug (2018)\u201d. url: https:\/\/www.bitcoinabc.org\/2018-05-07-incident-report\/."},{"key":"2026033014314832300_ref038","unstructured":"Chainlink\n            \n          . (2023). \u201cWhat Are Cross-Chain Smart Contracts?\u201d url: https:\/\/chain.link\/education-hub\/cross-chain-smart-contracts."},{"key":"2026033014314832300_ref039","unstructured":"ChainWall\n            \n          . (2023). \u201cReentrancy Attack in Smart Contracts\u201d. url: https:\/\/medium.com\/chainwall-io\/reentrancy-attack-in-smart-contracts-4837ed0f9d73."},{"issue":"1","key":"2026033014314832300_ref040","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0743-1066(85)90002-0","article-title":"Horn clause queries and generalizations","volume":"2","author":"Chandra","year":"1985","journal-title":"The Journal of Logic Programming"},{"key":"2026033014314832300_ref041","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1109\/EUROSP57164.2023.00028","volume-title":"8th IEEE European Symposium on Security and Privacy, EuroS&P 2023, Delft, Netherlands, July 3-7, 2023","author":"Chen","year":"2023"},{"key":"2026033014314832300_ref042","article-title":"Algorand","author":"Chen","year":"2016","journal-title":"arXiv preprint arXiv:1607.01341"},{"key":"2026033014314832300_ref043","article-title":"SODA: A Generic Online Detection Framework for Smart Contracts.","author":"Chen","year":"2020","journal-title":"NDSS"},{"key":"2026033014314832300_ref044","doi-asserted-by":"crossref","first-page":"2517","DOI":"10.1109\/SP46215.2023.10179386","volume-title":"2023 IEEE Symposium on Security and Privacy (SP)","author":"Chen","year":"2023"},{"key":"2026033014314832300_ref045","unstructured":"Chen, Z.\n           (2019). \u201cSmart Contract Reentrancy: TheDAO\u201d. url: https:\/\/medium.com\/@zhongqiangc\/smart-contract-reentrancy-thedao-f2da1d25180c."},{"key":"2026033014314832300_ref046","first-page":"227","article-title":"Smartian: Enhancing smart contract fuzzing with static and dynamic data-flow analyses","author":"Choi","year":"2021","journal-title":"2021 36th IEEE\/ACM International Conference on Automated Software Engineering (ASE)"},{"key":"2026033014314832300_ref047","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/BFb0058022","volume-title":"Foundations of Software Technology and Theoretical Computer Science: 17th Conference Kharagpur, India, December 18\u201320, 1997 Proceedings 17","author":"Clarke","year":"1997"},{"key":"2026033014314832300_ref048","first-page":"195","article-title":"Trace-based program analysis","author":"Colby","year":"1996","journal-title":"Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages"},{"key":"2026033014314832300_ref049","unstructured":"Consensus-Bug, G.\n           (2016). \u201cEthereum Geth Consensus Bug (2016)\u201d. url:https:\/\/\/2016\/11\/25\/security-alert-11242016-consensus-bug-geth-v1-4-19-v1-5-2\/."},{"key":"2026033014314832300_ref050","unstructured":"Cosmos\n            \n          . (2023). \u201cICS04: Something confusing about function timeout-Packet and timeoutOnClose\u201d. url:https:\/\/github.com\/cosmos\/ibc\/issues\/965."},{"key":"2026033014314832300_ref051","unstructured":"Cosmos\n          . (2024). \u201cInterchain Standards (ICS) for the Cosmos network & interchain ecosystem.\u201d url:https:\/\/github.com\/cosmos\/ibc."},{"key":"2026033014314832300_ref052","unstructured":"Cosmos Hub Forum\n          . (2024). \u201cEVM Precompiled contract bug allowing unlimited token mint\u201d. url:https:\/\/forum.cosmos.network\/t\/critical-evm-precompiled-contract-bug-allowing-unlimited-token-mint\/14060."},{"key":"2026033014314832300_ref053","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-642-32759-9_14","volume-title":"FM 2012: Formal Methods","author":"Cousineau","year":"2012"},{"key":"2026033014314832300_ref054","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1109\/SP40001.2021.00087","volume-title":"2021 IEEE Symposium on Security and Privacy (SP)","author":"Crain","year":"2021"},{"key":"2026033014314832300_ref055","first-page":"639","article-title":"VRust:Automated vulnerability detection for solana smart contracts","author":"Cui","year":"2022","journal-title":"Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security"},{"key":"2026033014314832300_ref056","unstructured":"CVE\n          . (2018). \u201cNVD - CVE-2018-11329\u201d. url:https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2018-11329."},{"key":"2026033014314832300_ref057","unstructured":"CWA-2023-004\n          . (2023). \u201cCWA-2023-004\u201d. url:https:\/\/github.com\/CosmWasm\/advisories\/blob\/main\/CWAs\/CWA-2023-004.md."},{"key":"2026033014314832300_ref058","unstructured":"Danila, R.\n           (2020). \u201cResponsible Vulnerability Disclosure\u201d. url: https:\/\/medium.com\/nexus-mutual\/responsible-vulnerability-disclosure-ece3fe3bcefa."},{"key":"2026033014314832300_ref059","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1109\/LICS.2001.932482","article-title":"Successive approximation of abstract transition relations","author":"Das","year":"2001","journal-title":"Proceedings 16th Annual IEEE Symposium on Logic in Computer Science"},{"issue":"1-2","key":"2026033014314832300_ref060","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/S1567-8326(02)00068-1","article-title":"Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes","volume":"56","author":"Desharnais","year":"2003","journal-title":"The Journal of Logic and Algebraic Programming"},{"key":"2026033014314832300_ref061","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1109\/SP61157.2025.00061","volume-title":"2025 IEEE Symposium on Security and Privacy (SP)","author":"Ding","year":"2025"},{"key":"2026033014314832300_ref062","unstructured":"Doshi, V.\n           (2023). \u201cTypes of attacks on smart contracts\u201d. url: https:\/\/varunx.hashnode.dev\/smart-contract-attack-vectors."},{"key":"2026033014314832300_ref063","doi-asserted-by":"crossref","DOI":"10.1145\/3377811.3380364","article-title":"Empirical review of automated analysis tools on 47,587 ethereum smart contracts","author":"Durieux","year":"2020","journal-title":"Proceedings of the ACM\/IEEE 42nd International conference on software engineering"},{"key":"2026033014314832300_ref064","unstructured":"Ethereum\n          . (2016). \u201cException on overflow\u201d. url: https:\/\/github.com\/ethereum\/solidity\/issues\/796%5C#issuecomment-253578925."},{"key":"2026033014314832300_ref065","unstructured":"Ethereum\n          . (2018). \u201cUtilities for interacting with the Ethereum virtual machine\u201d. url: https:\/\/github.com\/ethereum\/evmlab."},{"key":"2026033014314832300_ref066","unstructured":"Ethereum. (2020). \u201cGo Ethereum: Official Go implementation of the Ethereum protocol \u201d. url: https:\/\/github.com\/ethereum\/go-ethereum."},{"key":"2026033014314832300_ref067","unstructured":"Ethereum\n          . (2024a). \u201cCommon tests for all Ethereum implementations\u201d. url: https:\/\/github.com\/ethereum\/tests."},{"key":"2026033014314832300_ref068","unstructured":"Ethereum. (2024b). \u201cContract ABI Specification \u2014 Solidity 0.8.27 documentation\u201d. url: https:\/\/docs.soliditylang.org\/en\/latest\/abi-spec.html."},{"key":"2026033014314832300_ref069","unstructured":"Ethereum\n          . (2024c). \u201cERC-20 Token Standard\u201d. url: https:\/\/ethereum.org\/en\/developers\/docs\/standards\/tokens\/erc-20\/."},{"key":"2026033014314832300_ref070","unstructured":"Ethereum\n          . (2024d). \u201cSolidity 0.8.27 documentation\u201d. url:https:\/\/docs.soliditylang.org\/en\/v0.8.27\/."},{"key":"2026033014314832300_ref071","unstructured":"Ethereum\n          . (2024e). \u201cSolidity, the Smart Contract Programming Language\u201d. url: https:\/\/github.com\/ethereum\/solidity."},{"key":"2026033014314832300_ref072","unstructured":"Ethereum\n          . (2024f). \u201ctheRun Contract\u201d. url: https:\/\/etherscan.io\/address\/0xcac337492149bdb66b088bf5914bedfbf78ccc18%5C#code."},{"key":"2026033014314832300_ref073","article-title":"Ethereum (ETH) Blockchain Explorer","author":"Etherscan","year":"2024"},{"key":"2026033014314832300_ref074","unstructured":"Py-EVM\n          . (2024). \u201cA Python implementation of the Ethereum Virtual Machine\u201d. url:https:\/\/github.com\/ethereum\/py-evm."},{"key":"2026033014314832300_ref075","unstructured":"EVM\n          . (2024). \u201cEVM Codes - Precompiled Contracts\u201d. url: https:\/\/www.evm.codes\/precompiled."},{"key":"2026033014314832300_ref076","unstructured":"JS-EVM\n            \n          . (2024). \u201cTypeScript implementation of the Ethereum EVM.\u201d url:https:\/\/www.npmjs.com\/package\/@ethereumjs\/evm."},{"key":"2026033014314832300_ref077","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1109\/WETSEB.2019.00008","volume-title":"2019 IEEE\/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB)","author":"Feist","year":"2019"},{"key":"2026033014314832300_ref078","volume-title":"1st Summit on Advances in Programming Languages (SNAPL 2015)","author":"Felleisen","year":"2015"},{"key":"2026033014314832300_ref079","first-page":"1141","article-title":"Summary-based symbolic evaluation for smart contracts","author":"Feng","year":"2020","journal-title":"Proceedings of the 35th IEEE\/ACM International Conference on Automated Software Engineering"},{"key":"2026033014314832300_ref080","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings 22","author":"Filli\u00e2tre","year":"2013"},{"key":"2026033014314832300_ref081","unstructured":"Finance, B.\n           (2021). \u201cEconomic Exploit Attack on Bunny Protocol\u201d. url:https:\/\/pancakebunny.medium.com\/hello-bunny-fam-a7bf0c7a07ba."},{"issue":"2","key":"2026033014314832300_ref082","first-page":"1","article-title":"Dissecting american fuzzy lop: a fuzzbench evaluation","volume":"32","author":"Fioraldi","year":"2023","journal-title":"ACM transactions on software engineering and methodology"},{"key":"2026033014314832300_ref083","unstructured":"Flashbots\n          . (2024). \u201cFlashbots Docs\u201d. url: https:\/\/docs.flashbots.net\/flashbots-auction\/overview\/."},{"key":"2026033014314832300_ref084","unstructured":"Flaws, S.\n           (2024). \u201cSolidity compiler bugs\u201d. url:https:\/\/github.com\/ethereum\/solidity\/blob\/develop\/docs\/bugs.json."},{"key":"2026033014314832300_ref085","first-page":"1110","article-title":"Evmfuzzer: detect evm vulnerabilities via fuzz testing","author":"Fu","year":"2019","journal-title":"Proceedings of the 2019 27th ACM joint meeting on european software engineering conference and symposium on the foundations of software engineering"},{"key":"2026033014314832300_ref086","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/978-3-319-55559-1_2","article-title":"Labeled transition systems","author":"Gorrieri","year":"2017","journal-title":"Process Algebras for Petri Nets: The Alphabetization of Distributed Systems"},{"key":"2026033014314832300_ref087","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/978-3-642-24797-2_4","article-title":"Long short-term memory","author":"Graves","year":"2012","journal-title":"Supervised sequence labelling with recurrent neural networks"},{"key":"2026033014314832300_ref088","doi-asserted-by":"publisher","first-page":"116:1","DOI":"10.1145\/3276486","article-title":"MadMax: surviving out-of-gas conditions in Ethereum smart contracts","author":"Grech","year":"2018","journal-title":"Proc. ACM Program. Lang. 2(OOPSLA)"},{"key":"2026033014314832300_ref089","doi-asserted-by":"crossref","first-page":"557","DOI":"10.1145\/3395363.3404366","article-title":"Echidna: effective, usable, and fast fuzzing for smart contracts","author":"Grieco","year":"2020","journal-title":"Proceedings of the 29th ACM SIGSOFT international symposium on software testing and analysis"},{"key":"2026033014314832300_ref090","first-page":"243","volume-title":"Principles of Security and Trust: 7th International Conference, POST 2018, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings 7","author":"Grishchenko","year":"2018"},{"key":"2026033014314832300_ref091","first-page":"1793","article-title":"Confusum contractum: confused deputy vulnerabilities in ethereum smart contracts","author":"Gritti","year":"2023","journal-title":"32nd USENIX Security Symposium (USENIX Security 23)"},{"key":"2026033014314832300_ref092","unstructured":"Groce, A.\n           (2021). \u201cA Year in the Life of a Compiler Fuzzing Campaign\u201d. url: https:\/\/blog.trailofbits.com\/2021\/03\/23\/a-year-in-the-life-of-a-compiler-fuzzing-campaign\/."},{"key":"2026033014314832300_ref093","unstructured":"Groce, A.\n           (2024). \u201cVariation of american fuzzy lop for testing compilers\u201d. url: https:\/\/github.com\/agroce\/afl-compiler-fuzzer."},{"issue":"POPL","key":"2026033014314832300_ref094","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3158136","article-title":"Online detection of effectively callback free objects with applications to smart contracts","volume":"2","author":"Grossman","year":"2017","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"2026033014314832300_ref095","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1109\/SYNASC49474.2019.00010","article-title":"The science, art, and magic of constrained horn clauses","author":"Gurfinkel","year":"2019","journal-title":"2019 21st International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC)"},{"key":"2026033014314832300_ref096","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-18088-5_22","volume-title":"International Colloquium on Automata, Languages, and Programming","author":"Hafer","year":"1987"},{"key":"2026033014314832300_ref097","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-030-41600-3\\_11","volume-title":"Verified Software. Theories, Tools, and Experiments - 11th International Conference, VSTTE 2019,New York City, NY, USA, July 13-14, 2019, Revised Selected Papers","author":"Hajdu","year":"2019"},{"key":"2026033014314832300_ref098","volume-title":"Return to First Principles","author":"Hallberg","year":"2012"},{"key":"2026033014314832300_ref099","unstructured":"Harbor\n          . (2023). \u201cEdition of series on security audits: Risk of precompiled contracts\u201d. url:https:\/\/medium.com\/coinmonks\/edition-of-series-on-security-audits-risk-of-precompiled-contracts-c99b64006cef."},{"key":"2026033014314832300_ref100","unstructured":"Harper, C.\n           (2020). \u201cEthereum\u2019s \u2018Unannounced Hard Fork\u2019 Was Trying to Prevent the Very Disruption It Caused\u201d. url:https:\/\/www.coindesk.com\/tech\/2020\/11\/11\/ethereums-unannounced-hard-fork-was-trying-to-prevent-the-very-disruption-it-caused."},{"key":"2026033014314832300_ref101","first-page":"1","article-title":"Probabilistic temporal logics for finite and bounded models","author":"Hart","year":"1984","journal-title":"Proceedings of the sixteenth annual ACM symposium on Theory of computing"},{"key":"2026033014314832300_ref102","article-title":"Towards safer smart contracts: A survey of languages and verification methods","author":"Harz","year":"2018","journal-title":"arXiv preprint arXiv:1809.09805"},{"key":"2026033014314832300_ref103","first-page":"531","article-title":"Learning to fuzz from symbolic execution with application to smart contracts","author":"He","year":"2019","journal-title":"Proceedings of the 2019 ACM SIGSAC conference on computer and communications security"},{"key":"2026033014314832300_ref104","first-page":"1271","article-title":"{EOSAFE}: security analysis of {EOSIO} smart contracts","author":"He","year":"2021","journal-title":"30th USENIX security symposium (USENIX Security 21)"},{"key":"2026033014314832300_ref105","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1109\/CSF.2018.00022","volume-title":"2018 IEEE 31st Computer Security Foundations Symposium (CSF)","author":"Hildenbrandt","year":"2018"},{"key":"2026033014314832300_ref106","doi-asserted-by":"crossref","first-page":"520","DOI":"10.1007\/978-3-319-70278-0_33","volume-title":"Financial Cryptography and Data Security: FC 2017 International Workshops, WAHC, BITCOIN, VOTING, WTSC, and TA, Sliema, Malta, April 7, 2017, Revised Selected Papers 21","author":"Hirai","year":"2017"},{"issue":"8","key":"2026033014314832300_ref107","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","article-title":"Communicating sequential processes","volume":"21","author":"Hoare","year":"1978","journal-title":"Communications of the ACM"},{"key":"2026033014314832300_ref108","first-page":"1","article-title":"Revealing Hidden Threats: An Empirical Study of Library Misuse in Smart Contracts","author":"Huang","year":"2024","journal-title":"Proceedings of the 46th IEEE\/ACM International Conference on Software Engineering"},{"key":"2026033014314832300_ref109","article-title":"The coq proof assistant a tutorial","author":"Huet","year":"1997","journal-title":"Rapport Technique"},{"key":"2026033014314832300_ref110","first-page":"1","article-title":"Smart contract modeling and verification techniques: A survey","author":"Imeri","year":"2020","journal-title":"8th International Workshop on ADVANCEs in ICT Infrastructures and Services (ADVANCE 2020)"},{"key":"2026033014314832300_ref111","unstructured":"Immunefi\n          . (2023). \u201cCommon Cross-Chain Bridge Vulnerabilities\u201d. url:https:\/\/medium.com\/immunefi\/common-cross-chain-bridge-vulnerabilities-d8c161ffaf8f."},{"key":"2026033014314832300_ref112","unstructured":"Inspex\n          . (2022). \u201cCross-Contract Reentrancy Attack\u201d. url: https:\/\/inspexco.medium.com\/cross-contract-reentrancy-attack-402d27a02a15."},{"key":"2026033014314832300_ref113","unstructured":"Iosiro\n          . (2024). \u201cGeth Out-of-Order EIP Application Denial-of-Service \u201d.url:https:\/\/iosiro.com\/blog\/geth-out-of-order-eip-application-denial-of-service."},{"key":"2026033014314832300_ref114","first-page":"24","article-title":"A process calculus for formally verifying blockchain consensus protocols","author":"Jeltsch","year":"2019","journal-title":"International Conference on Applications of Declarative Programming and Knowledge Management"},{"key":"2026033014314832300_ref115","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1145\/3238147.3238177","article-title":"Contractfuzzer: Fuzzing smart contracts for vulnerability detection","author":"Jiang","year":"2018","journal-title":"Proceedings of the 33rd ACM\/IEEE international conference on automated software engineering"},{"key":"2026033014314832300_ref116","doi-asserted-by":"crossref","first-page":"1695","DOI":"10.1109\/SP40000.2020.00066","article-title":"Semantic understanding of smart contracts: Executable operational semantics of solidity","author":"Jiao","year":"2020","journal-title":"2020 IEEE Symposium on Security and Privacy (SP)"},{"key":"2026033014314832300_ref117","doi-asserted-by":"crossref","DOI":"10.1145\/3643895","article-title":"A Survey of Ethereum Smart Contract Security: Attacks and Detection","author":"Jiao","year":"2024","journal-title":"Distributed Ledger Technologies: Research and Practice"},{"key":"2026033014314832300_ref118","doi-asserted-by":"publisher","first-page":"4:1","DOI":"10.4230\/OASICS.FMBC.2024.4","volume-title":"5th International Workshop on Formal Methods for Blockchains, FMBC 2024, April 7, 2024, Luxembourg City, Luxembourg","author":"Jones","year":"2024"},{"key":"2026033014314832300_ref119","first-page":"422","volume-title":"Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II 28","author":"Jordan","year":"2016"},{"key":"2026033014314832300_ref120","article-title":"Speech and Language Processing: An Introduction to Natural Language Processing, Computational Linguistics, and Speech Recognition","author":"Jurafsky","year":"2024"},{"key":"2026033014314832300_ref121","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1109\/PERCOMWORKSHOPS56833.2023.10150389","volume-title":"IEEE International Conference on Pervasive Computing and Communications Workshops and other Affiliated Events, PerCom Workshops 2023, Atlanta, GA, USA, March 13-17, 2023","author":"Kado","year":"2023"},{"key":"2026033014314832300_ref122","first-page":"1","article-title":"Zeus: analyzing safety of smart contracts.","author":"Kalra","year":"2018","journal-title":"Ndss"},{"key":"2026033014314832300_ref123","first-page":"69","volume-title":"2020 Indo\u2013Taiwan 2nd International Conference on Computing, Analytics and Networks (Indo-Taiwan ICAN)","author":"Ke","year":"2020"},{"key":"2026033014314832300_ref124","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1145\/3465084.3467905","article-title":"All you need is dag","author":"Keidar","year":"2021","journal-title":"Proceedings of the 2021 ACM Symposium on Principles of Distributed Computing"},{"key":"2026033014314832300_ref125","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","article-title":"SMT-based model checking for recursive programs","volume":"48","author":"Komuravelli","year":"2016","journal-title":"Formal Methods in System Design"},{"key":"2026033014314832300_ref126","doi-asserted-by":"crossref","first-page":"1144","DOI":"10.1145\/3597926.3598124","article-title":"Defitainter: Detecting price manipulation vulnerabilities in defi protocols","author":"Kong","year":"2023","journal-title":"Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis"},{"key":"2026033014314832300_ref127","doi-asserted-by":"crossref","first-page":"719","DOI":"10.1145\/3009837.3009860","article-title":"A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms","author":"Konnov","year":"2017","journal-title":"Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"},{"issue":"5","key":"2026033014314832300_ref128","doi-asserted-by":"crossref","first-page":"583","DOI":"10.3233\/JCS-160556","article-title":"Automated analysis of security protocols with global state","volume":"24","author":"Kremer","year":"2016","journal-title":"Journal of Computer Security"},{"key":"2026033014314832300_ref129","unstructured":"Krishna, A.\n           (2024). \u201cBlockchain Security Issues: A Complete Guide\u201d. url: https:\/\/www.getastra.com\/blog\/knowledge-base\/blockchain-security-issues\/."},{"key":"2026033014314832300_ref130","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/s10009-004-0140-2","article-title":"Probabilistic symbolic model checking with PRISM: A hybrid approach","volume":"6","author":"Kwiatkowska","year":"2004","journal-title":"International journal on software tools for technology transfer"},{"key":"2026033014314832300_ref131","doi-asserted-by":"crossref","first-page":"1691","DOI":"10.1109\/ALLERTON.2010.5707120","article-title":"Advances and challenges of probabilistic model checking","author":"Kwiatkowska","year":"2010","journal-title":"2010 48th Annual Allerton Conference on Communication, Control, and Computing (Allerton)"},{"key":"2026033014314832300_ref132","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/1882362.1882405","article-title":"Differential static analysis: Opportunities, applications, and challenges","author":"Lahiri","year":"2010","journal-title":"Proceedings of the FSE\/SDP workshop on Future of software engineering research"},{"key":"2026033014314832300_ref133","first-page":"657","article-title":"What good is temporal logic?","author":"Lamport","year":"1983","journal-title":"IFIP congress"},{"key":"2026033014314832300_ref134","unstructured":"Lamport, L.\n           (2021). \u201cA High-Level View of TLA+\u201d. url: https:\/\/lamport.azurewebsites.net\/tla\/high-level-view.html."},{"key":"2026033014314832300_ref135","article-title":"A Formal Analysis of Blockchain Consensus","author":"Laneve","year":"2020","journal-title":"AFABC. pdf"},{"key":"2026033014314832300_ref136","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","article-title":"UPPAAL in a nutshell","volume":"1","author":"Larsen","year":"1997","journal-title":"International journal on software tools for technology transfer"},{"key":"2026033014314832300_ref137","doi-asserted-by":"crossref","first-page":"43620","DOI":"10.1109\/ACCESS.2021.3065880","article-title":"A comprehensive review of block-chain consensus mechanisms","volume":"9","author":"Lashkari","year":"2021","journal-title":"IEEE access"},{"key":"2026033014314832300_ref138","doi-asserted-by":"crossref","first-page":"918","DOI":"10.1109\/PADSW.2018.8645001","volume-title":"2018 IEEE 24th International Conference on Parallel and Distributed Systems (ICPADS)","author":"Laszka","year":"2018"},{"issue":"2","key":"2026033014314832300_ref139","doi-asserted-by":"publisher","first-page":"984","DOI":"10.1109\/TR.2022.3161634","article-title":"ReDefender: Detecting Reentrancy Vulnerabilities in Smart Contracts Automatically","volume":"71","author":"Li","year":"2022","journal-title":"IEEE Trans. Reliab"},{"key":"2026033014314832300_ref140","doi-asserted-by":"crossref","DOI":"10.1145\/3581784.3607053","article-title":"Fisco-bcos: An enterprise-grade permissioned blockchain system with high-performance","author":"Li","year":"2023","journal-title":"Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis"},{"key":"2026033014314832300_ref141","doi-asserted-by":"crossref","unstructured":"Li, K., J.Chen, X.Liu, Y. R.Tang, X.Wang, and X.Luo. (2021a). \u201cAs Strong As Its Weakest Link: How to Break Blockchain DApps at RPC Service\u201d. In: 28th Annual Network and Distributed System Security Symposium, NDSS 2021, virtually, February 21-25, 2021. The Internet Society. url:https:\/\/www.ndss-symposium.org\/ndss-paper\/as-strong-as-its-weakest-link-how-to-break-blockchain-dapps-at-rpc-service\/.","DOI":"10.14722\/ndss.2021.23108"},{"key":"2026033014314832300_ref142","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1145\/3487552.3487814","volume-title":"IMC \u201921: ACM Internet Measurement Conference, Virtual Event, USA, November 2-4, 2021","author":"Li","year":"2021"},{"key":"2026033014314832300_ref143","doi-asserted-by":"publisher","first-page":"1645","DOI":"10.1145\/3460120.3485369","volume-title":"CCS \u201921: 2021 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15 - 19, 2021","author":"Li","year":"2021"},{"key":"2026033014314832300_ref144","doi-asserted-by":"publisher","first-page":"1847","DOI":"10.1145\/3589334.3645640","volume-title":"Proceedings of the ACM on Web Conference 2024, WWW 2024, Singapore, May 13-17, 2024","author":"Li","year":"2024"},{"key":"2026033014314832300_ref145","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1109\/BIGCOM.2019.00021","volume-title":"2019 5th International Conference on Big Data Computing and Communications (BIGCOM)","author":"Li","year":"2019"},{"issue":"FSE","key":"2026033014314832300_ref146","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1145\/3643738","article-title":"SmartAxe: Detecting Cross-Chain Vulnerabilities in Bridge Smart Contracts via Fine-Grained Static Analysis","volume":"1","author":"Liao","year":"2024","journal-title":"Proceedings of the ACM on Software Engineering"},{"key":"2026033014314832300_ref147","first-page":"65","article-title":"Reguard: finding reentrancy bugs in smart contracts","author":"Liu","year":"2018","journal-title":"Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings"},{"key":"2026033014314832300_ref148","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1109\/Blockchain62396.2024.00021","volume-title":"2024 IEEE International Conference on Blockchain (Blockchain)","author":"Luo","year":"2024"},{"key":"2026033014314832300_ref149","unstructured":"Lutz, O., H.Chen, H.Fereidooni, C.Sendner, A.Dmitrienko, A. R.Sadeghi, and F.Koushanfar. (2021). \u201cESCORT: Ethereum Smart COntRacTs Vulnerability Detection using Deep Neural Network and Transfer Learning\u201d. url: https:\/\/arxiv.org\/abs\/2103.12607."},{"key":"2026033014314832300_ref150","first-page":"254","article-title":"Making smart contracts smarter","author":"Luu","year":"2016","journal-title":"Proceedings of the 2016 ACM SIGSAC conference on computer and communications security"},{"key":"2026033014314832300_ref151","doi-asserted-by":"crossref","unstructured":"Ma, F., Y.Chen, M.Ren, Y.Zhou, Y.Jiang, T.Chen, H.Li, and J.Sun. (2023). \u201cLOKI: State-Aware Fuzzing Framework for the Implementation of Blockchain Consensus Protocols\u201d. In: 30th Annual Network and Distributed System Security Symposium, NDSS 2023, San Diego, California, USA, February 27 - March 3, 2023. The Internet Society. url: https:\/\/www.ndss-symposium.org\/ndss-paper\/loki-state-aware-fuzzing-framework-for-the-implementation-of-blockchain-consensus-protocols\/.","DOI":"10.14722\/ndss.2023.24078"},{"key":"2026033014314832300_ref152","doi-asserted-by":"publisher","first-page":"1312","DOI":"10.1145\/3650212.3680362","volume-title":"Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2024, Vienna, Austria, September 16-20, 2024","author":"Ma","year":"2024"},{"key":"2026033014314832300_ref153","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1145\/3503921.3503923","article-title":"Uncovering Smart Contract VM Bugs Via Differential Fuzzing","author":"Maier","year":"2021","journal-title":"Reversing and Offensive-oriented Trends Symposium"},{"key":"2026033014314832300_ref154","first-page":"523","volume-title":"Financial Cryptography and Data Security: 22nd International Conference, FC 2018, Nieuwpoort, Cura\u00e7ao, February 26\u2013March 2, 2018, Revised Selected Papers 22","author":"Mavridou","year":"2018"},{"key":"2026033014314832300_ref155","doi-asserted-by":"crossref","first-page":"446","DOI":"10.1007\/978-3-030-32101-7_27","volume-title":"Financial Cryptography and Data Security: 23rd International Conference, FC 2019, Frigate Bay, St. Kitts and Nevis, February 18\u201322, 2019, Revised Selected Papers 23","author":"Mavridou","year":"2019"},{"key":"2026033014314832300_ref156","first-page":"1","article-title":"The stellar consensus protocol: A federated model for internet-level consensus","volume":"32","author":"Mazieres","year":"2015","journal-title":"Stellar Development Foundation"},{"issue":"1","key":"2026033014314832300_ref157","first-page":"100","article-title":"Differential testing for software","volume":"10","author":"McKeeman","year":"1998","journal-title":"Digital Technical Journal"},{"key":"2026033014314832300_ref158","doi-asserted-by":"crossref","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification: 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 25","author":"Meier","year":"2013"},{"key":"2026033014314832300_ref159","doi-asserted-by":"crossref","unstructured":"Meisami, S., H.Dabadie, S.Li, Y.Tang, and Y.Duan. (2025). \u201cSigScope: Detecting and Understanding Off-Chain Message Signing-related Vulnerabilities in Decentralized Applications\u201d.In: THE WEB CONFERENCE 2025. url:https:\/\/openreview.net\/forum?id=8OIqXq455O.","DOI":"10.1145\/3696410.3714686"},{"key":"2026033014314832300_ref160","article-title":"Analysis of mutation and generation-based fuzzing","author":"Miller","year":"2007","journal-title":"Independent Security Evaluators, Tech. Rep. 4"},{"key":"2026033014314832300_ref161","unstructured":"Monarch\n          . (2017). \u201cKing of the Ether\u201d.url:https:\/\/www.kingoftheether.com\/thrones\/kingoftheether\/index.html."},{"key":"2026033014314832300_ref162","doi-asserted-by":"crossref","first-page":"1186","DOI":"10.1109\/ASE.2019.00133","volume-title":"2019 34th IEEE\/ACM International Conference on Automated Software Engineering (ASE)","author":"Mossberg","year":"2019"},{"key":"2026033014314832300_ref163","article-title":"Mythril: security analysis tool for evm bytecode","author":"Mueller","year":"2017"},{"issue":"9","key":"2026033014314832300_ref164","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1145\/2692915.2628143","article-title":"Lem: reusable engineering of real-world semantics","volume":"49","author":"Mulligan","year":"2014","journal-title":"ACM SIGPLAN Notices"},{"key":"2026033014314832300_ref165","first-page":"1","volume-title":"2019 10th IFIP International Conference on New Technologies, Mobility and Security (NTMS)","author":"Murray","year":"2019"},{"key":"2026033014314832300_ref166","unstructured":"Nakamoto, S.\n           (2008). \u201cBitcoin: A Peer-to-Peer Electronic Cash System\u201d. url:https:\/\/bitcoin.org\/bitcoin.pdf."},{"key":"2026033014314832300_ref167","doi-asserted-by":"crossref","unstructured":"Neha\u00ed, Z., F.Bobot, S.Tucci-Piergiovanni, C.Delporte-Gallet, and H.Fauconnier. (2022). \u201cA tla+ formal proof of a cross-chain swap\u201d. In: Proceedings of the 23rd International Conference on Distributed Computing and Networking. 148\u2013159.","DOI":"10.1145\/3491003.3491006"},{"key":"2026033014314832300_ref168","unstructured":"Neo\n          . (2024). \u201cNeoVM - NEO Developer Resource\u201d. url: https:\/\/developers.neo.org\/docs\/n3\/foundation\/neovm."},{"key":"2026033014314832300_ref169","unstructured":"Nervos\n            \n          . (2024). \u201cCKB Consensus\u201d. url: https:\/\/docs-old.nervos.org\/docs\/basics\/concepts\/consensus."},{"key":"2026033014314832300_ref170","doi-asserted-by":"crossref","first-page":"1215","DOI":"10.1109\/SP40001.2021.00057","volume-title":"2021 IEEE Symposium on Security and Privacy (SP)","author":"Nguyen","year":"2021"},{"key":"2026033014314832300_ref171","doi-asserted-by":"crossref","first-page":"778","DOI":"10.1145\/3377811.3380334","article-title":"sfuzz: An efficient adaptive fuzzer for solidity smart contracts","author":"Nguyen","year":"2020","journal-title":"Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering"},{"key":"2026033014314832300_ref172","first-page":"380","volume-title":"International Symposium on Formal Methods","author":"Nielsen","year":"2019"},{"key":"2026033014314832300_ref173","volume-title":"Principles of program analysis","author":"Nielson","year":"2015"},{"key":"2026033014314832300_ref174","doi-asserted-by":"publisher","first-page":"653","DOI":"10.1145\/3274694.3274743","volume-title":"Proceedings of the 34th Annual Computer Security Applications Conference, ACSAC 2018, San Juan, PR, USA, December 03-07, 2018","author":"Nikolic","year":"2018"},{"key":"2026033014314832300_ref175","unstructured":"NIST\n            \n          . (2018). \u201cCVE-2018-10376 Detail\u201d. url: https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2018-10376."},{"key":"2026033014314832300_ref176","unstructured":"NIST\n            \n          . (2020a). \u201cNVD - CVE-2020-26241\u201d. url: https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2020-26241."},{"key":"2026033014314832300_ref177","unstructured":"NIST\n          . (2020b). \u201cNVD - CVE-2020-26265\u201d. url: https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2020-26265."},{"key":"2026033014314832300_ref178","unstructured":"NIST\n          . (2021). \u201cNVD - CVE-2021-39137\u201d. url: https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2021-39137."},{"key":"2026033014314832300_ref179","unstructured":"NIST\n          . (2022). \u201cNVD - CVE-2022-26534\u201d. url: https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2022-26534."},{"key":"2026033014314832300_ref180","article-title":"Math - OpenZeppelin Docs","author":"OpenZeppelin","year":"2024"},{"key":"2026033014314832300_ref181","unstructured":"Palladino, S.\n           (2017). \u201cThe Parity Wallet Hack Explained\u201d. url: https:\/\/blog.openzeppelin.com\/on-the-parity-wallet-multisig-hack-405a8c12e8f7."},{"key":"2026033014314832300_ref182","unstructured":"Pcaversaccio\n          . (2024). \u201cA chronological and (hopefully) complete list of reentrancy attacks to date.\u201d url: https:\/\/github.com\/pcaversaccio\/reentrancy-attacks?tab=readme-ov-file."},{"key":"2026033014314832300_ref183","doi-asserted-by":"crossref","first-page":"1661","DOI":"10.1109\/SP40000.2020.00024","volume-title":"2020 IEEE symposium on security and privacy (SP)","author":"Permenev","year":"2020"},{"key":"2026033014314832300_ref184","first-page":"249","volume-title":"International Conference on Formal Engineering Methods","author":"Pillai","year":"2023"},{"key":"2026033014314832300_ref185","article-title":"A structural approach to operational semantics","author":"Plotkin","year":"1981"},{"issue":"7","key":"2026033014314832300_ref186","first-page":"579","article-title":"Multilayer perceptron and neural networks","volume":"8","author":"Popescu","year":"2009","journal-title":"WSEAS Transactions on Circuits and Systems"},{"key":"2026033014314832300_ref187","article-title":"Security analysis methods on ethereum smart contract vulnerabilities: a survey","author":"Praitheeshan","year":"2019","journal-title":"arXiv preprint arXiv:1908.08605"},{"issue":"7","key":"2026033014314832300_ref188","doi-asserted-by":"crossref","first-page":"578","DOI":"10.1093\/comjnl\/38.7.578","article-title":"Stochastic \u03c0-calculus","volume":"38","author":"Priami","year":"1995","journal-title":"The Computer Journal"},{"key":"2026033014314832300_ref189","doi-asserted-by":"publisher","first-page":"5:1","DOI":"10.4230\/OASICS.FMBC.2024.5","volume-title":"5th International Workshop on Formal Methods for Blockchains, FMBC 2024, April 7, 2024, Luxembourg City, Luxembourg","author":"Pusceddu","year":"2024"},{"key":"2026033014314832300_ref190","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1016\/S0927-0507(05)80172-0","article-title":"Markov decision processes","volume":"2","author":"Puterman","year":"1990","journal-title":"Handbooks in operations research and management science"},{"key":"2026033014314832300_ref191","article-title":"Smart contract vulnerability detection technique: A survey","author":"Qian","year":"2022","journal-title":"arXiv preprint arXiv:2209.05872"},{"key":"2026033014314832300_ref192","first-page":"3961","article-title":"The blockchain imitation game","author":"Qin","year":"2023","journal-title":"32nd USENIX Security Symposium (USENIX Security 23)"},{"key":"2026033014314832300_ref193","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-662-64322-8\\_1","volume-title":"Financial Cryptography and Data Security - 25th International Conference, FC 2021, Virtual Event, March 1-5, 2021, Revised Selected Papers, Part I","author":"Qin","year":"2021"},{"key":"2026033014314832300_ref194","volume-title":"Proceedings 2019 Network and Distributed System Security Symposium","author":"Rodler","year":"2019"},{"key":"2026033014314832300_ref195","first-page":"1289","article-title":"{EVMPatch}: Timely and automated patching of ethereum smart contracts","author":"Rodler","year":"2021","journal-title":"30th usenix security symposium (USENIX Security 21)"},{"issue":"6","key":"2026033014314832300_ref196","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","article-title":"An overview of the K semantic framework","volume":"79","author":"Ro\u015fu","year":"2010","journal-title":"The Journal of Logic and Algebraic Programming"},{"key":"2026033014314832300_ref197","doi-asserted-by":"crossref","DOI":"10.14722\/ndss.2024.24713","article-title":"Not your Type! Detecting Storage Collision Vulnerabilities in Ethereum Smart Contracts","author":"Ruaro","year":"2024","journal-title":"Proceedings of the Network and Distributed System Security (NDSS) Symposium"},{"key":"2026033014314832300_ref198","doi-asserted-by":"crossref","DOI":"10.14722\/ndss.2024.24713","article-title":"Not your Type! Detecting Storage Collision Vulnerabilities in Ethereum Smart Contracts","author":"Ruaro","year":"2024","journal-title":"Netw. Distrib. Syst. Security Symp"},{"key":"2026033014314832300_ref199","first-page":"73","article-title":"A survey of security vulnerabilities in ethereum smart contracts","author":"Samreen","year":"2020","journal-title":"Proceedings of the 30th Annual International Conference on Computer Science and Software Engineering"},{"key":"2026033014314832300_ref200","article-title":"A survey of security vulnerabilities in ethereum smart contracts","author":"Samreen","year":"2021","journal-title":"arXiv preprint arXiv:2105.06974"},{"key":"2026033014314832300_ref201","first-page":"621","article-title":"ethor: Practical and provably sound static analysis of ethereum smart contracts","author":"Schneidewind","year":"2020","journal-title":"Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security"},{"key":"2026033014314832300_ref202","unstructured":"Secure3\n          . (2023). \u201cAnalysis of the Blockchain Security Chain Events Caused by Vyper Compiler Vulnerabilities\u201d. url: https:\/\/medium.com\/@Secure3\/analysis-of-the-blockchain-security-chain-events-caused-by-vyper-compiler-vulnerabilities-37b66ad8aa45."},{"key":"2026033014314832300_ref203","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","volume-title":"Computer Aided Verification: 16th International Conference, CAV 2004, Boston, MA, USA, July 13-17, 2004. Proceedings 16","author":"Sen","year":"2004"},{"key":"2026033014314832300_ref204","doi-asserted-by":"crossref","unstructured":"Sendner, C., H.Chen, H.Fereidooni, L.Petzi, J.K\u00f6nig, J.Stang, A.Dmitrienko, A.-R.Sadeghi, and F.Koushanfar. (2023). \u201cSmarter Contracts: Detecting Vulnerabilities in Smart Contracts with Deep Transfer Learning.\u201d In: NDSS.","DOI":"10.14722\/ndss.2023.23263"},{"key":"2026033014314832300_ref205","article-title":"Mastering Delegatecall in Solidity: A Comprehensive Guide with EVM Walkthrough","author":"Serah","year":"2023"},{"key":"2026033014314832300_ref206","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/SecDev.2016.043","volume-title":"2016 IEEE Cybersecurity Development (SecDev)","author":"Serebryany","year":"2016"},{"key":"2026033014314832300_ref207","unstructured":"SlowMist\n          . (2021). \u201cThe Analysis and Q&A Of Poly Network Being Hacked\u201d. url: https:\/\/slowmist.medium.com\/the-analysis-and-q-a-of-poly-network-being-hacked-8112a35beb39."},{"key":"2026033014314832300_ref208","unstructured":"Smith, C.\n           (2024). \u201cProof-of-stake (PoS)\u201d. url: https:\/\/ethereum.org\/en\/developers\/docs\/consensus-mechanisms\/pos\/."},{"key":"2026033014314832300_ref209","first-page":"1197","article-title":"Fuzz on the beach: Fuzzing solana smart contracts","author":"Smolka","year":"2023","journal-title":"Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security"},{"key":"2026033014314832300_ref210","first-page":"1361","article-title":"{SmarTest}: Effectively hunting vulnerable transaction sequences in smart contracts through language {Model-Guided} symbolic execution","author":"So","year":"2021","journal-title":"30th USENIX Security Symposium (USENIX Security 21)"},{"key":"2026033014314832300_ref211","doi-asserted-by":"crossref","first-page":"1678","DOI":"10.1109\/SP40000.2020.00032","volume-title":"2020 IEEE Symposium on Security and Privacy (SP)","author":"So","year":"2020"},{"key":"2026033014314832300_ref212","unstructured":"SOL-2020-5\n          . (2024). \u201cSolidity compiler flaw SOL-2020-5\u201d. url: https:\/\/github.com\/ethereum\/solidity\/blob\/develop\/docs\/bugs.json\/%5C#L224."},{"key":"2026033014314832300_ref213","unstructured":"Solidity\n          . (2024a). \u201cFunction Modifiers\u201d. url: https:\/\/docs.soliditylang.org\/en\/latest\/contracts.html%5C#function-modifiers."},{"key":"2026033014314832300_ref214","unstructured":"Solidity\n          . (2024b). \u201cSending Ether (transfer, send, call)\u201d. url: https:\/\/solidity-by-example.org\/sending-ether\/."},{"key":"2026033014314832300_ref215","unstructured":"Solidity\n          . (2024c). \u201cSolidity, the Smart Contract Programming Language\u201d. url: https:\/\/github.com\/ethereum\/solidity."},{"key":"2026033014314832300_ref216","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1109\/SP40001.2021.00085","volume-title":"2021 IEEE Symposium on Security and Privacy (SP)","author":"Stephens","year":"2021"},{"key":"2026033014314832300_ref217","first-page":"1307","article-title":"Evil under the sun: Understanding and discovering attacks on ethereum decentralized applications","author":"Su","year":"2021","journal-title":"30th USENIX Security Symposium (USENIX Security 21)"},{"key":"2026033014314832300_ref218","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1109\/TASE.2009.32","volume-title":"2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering","author":"Sun","year":"2009"},{"key":"2026033014314832300_ref219","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification: 21st International Conference, CAV 2009, Grenoble, France, June 26-July 2, 2009. Proceedings 21","author":"Sun","year":"2009"},{"issue":"22","key":"2026033014314832300_ref220","doi-asserted-by":"crossref","first-page":"2954","DOI":"10.3390\/math9222954","article-title":"Modeling and verifying the CKB blockchain consensus protocol","volume":"9","author":"Sun","year":"2021","journal-title":"Mathematics"},{"issue":"2","key":"2026033014314832300_ref221","doi-asserted-by":"crossref","first-page":"255","DOI":"10.3390\/electronics9020255","article-title":"A formal verification framework for security issues of blockchain smart contracts","volume":"9","author":"Sun","year":"2020","journal-title":"Electronics"},{"key":"2026033014314832300_ref222","first-page":"1","article-title":"Gptscan: Detecting logic vulnerabilities in smart contracts by combining gpt with program analysis","author":"Sun","year":"2024","journal-title":"Proceedings of the IEEE\/ACM 46th International Conference on Software Engineering"},{"key":"2026033014314832300_ref223","unstructured":"SWC\n          . (2024). \u201cSWC-115 - Smart Contract Weakness Classification (SWC)\u201d. url: https:\/\/swcregistry.io\/docs\/SWC-115\/."},{"key":"2026033014314832300_ref224","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1109\/ICECCS2018.2018.00031","volume-title":"2018 23rd International Conference on Engineering of Complex Computer Systems (ICECCS)","author":"Thin","year":"2018"},{"key":"2026033014314832300_ref225","unstructured":"Thummavet, P.\n           (2022). \u201cSolidity Security By Example #04: Cross-Function Reentrancy\u201d. url: https:\/\/medium.com\/valixconsulting\/solidity-smart-contract-security-by-example-04-cross-function-reentrancy-de9cbce0558e."},{"key":"2026033014314832300_ref226","first-page":"1","article-title":"Differential testing solidity compiler through deep contract manipulation and mutation","author":"Tian","year":"2024","journal-title":"Software Quality Journal"},{"issue":"7","key":"2026033014314832300_ref227","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3464421","article-title":"A survey of smart contract formal specification and verification","volume":"54","author":"Tolmach","year":"2021","journal-title":"ACM Computing Surveys (CSUR)"},{"key":"2026033014314832300_ref228","first-page":"67","article-title":"Securify: Practical security analysis of smart contracts","author":"Tsankov","year":"2018","journal-title":"Proceedings of the 2018 ACM SIGSAC conference on computer and communications security"},{"key":"2026033014314832300_ref229","article-title":"Principles of database and knowledge-base systems","author":"Ullman Jeffrey","year":"1988"},{"key":"2026033014314832300_ref230","unstructured":"Verge\n          . (2018). \u201cVerge (XVG) Time-Warp Exploit (2018)\u201d. url: https:\/\/www.reddit.com\/r\/CryptoCurrency\/comments\/avvmb9\/verge_xvg_has_lost_94_percent_of_its_value_after\/."},{"key":"2026033014314832300_ref231","doi-asserted-by":"crossref","first-page":"66611","DOI":"10.1109\/ACCESS.2022.3184799","article-title":"Introduction of formal methods in blockchain consensus mechanism and its associated protocols","volume":"10","author":"Verma","year":"2022","journal-title":"IEEE Access"},{"key":"2026033014314832300_ref232","unstructured":"Veschetti, A.\n           (2022). \u201cSource Code of PRISM+\u201d. url: https:\/\/github.com\/adeleveschetti\/bitcoin-analysis\/tree\/master."},{"key":"2026033014314832300_ref233","unstructured":"Veschetti, A.\n           (2023). \u201cA formal analysis of blockchain consensus\u201d. url: http:\/\/amsdottorato.unibo.it\/10835\/."},{"key":"2026033014314832300_ref234","unstructured":"Vyper\n            \n          . (2024). \u201cCompiling a Contract\u201d. url: https:\/\/docs.vyperlang.org\/en\/stable\/compiling-a-contract.html."},{"key":"2026033014314832300_ref235","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1109\/MSR.2017.59","volume-title":"Proceedings of the 14th International Conference on Mining Software Repositories, MSR 2017, Buenos Aires, Argentina, May 20-28, 2017","author":"Wan","year":"2017"},{"key":"2026033014314832300_ref236","first-page":"23","article-title":"Towards a first step to understand flash loan and its applications in defi ecosystem","author":"Wang","year":"2021","journal-title":"Proceedings of the Ninth International Workshop on Security in Blockchain and Cloud Computing"},{"key":"2026033014314832300_ref237","volume-title":"PhD thesis","author":"Wang","year":"2019"},{"issue":"OOPSLA","key":"2026033014314832300_ref238","first-page":"1","article-title":"Detecting nondeterministic payment bugs in ethereum smart contracts","volume":"3","author":"Wang","year":"2019","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"2026033014314832300_ref239","first-page":"3367","article-title":"Automated inference on financial security of Ethereum smart contracts","author":"Wang","year":"2023","journal-title":"32nd USENIX Security Symposium (USENIX Security 23)"},{"key":"2026033014314832300_ref240","volume-title":"33rd USENIX Security Symposium, USENIX Security 2024, Philadelphia, PA, USA, August 14-16, 2024","author":"Wang","year":"2024"},{"key":"2026033014314832300_ref241","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1145\/3468264.3468568","volume-title":"ESEC\/FSE \u201921: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Athens, Greece, August 23-28, 2021","author":"Wang","year":"2021"},{"key":"2026033014314832300_ref242","first-page":"1","volume-title":"2023 IEEE 31st International Conference on Network Protocols (ICNP)","author":"Wei","year":"2023"},{"key":"2026033014314832300_ref243","first-page":"119","article-title":"The tableau method for temporal logic: An overview","author":"Wolper","year":"1985","journal-title":"Logique et Analyse"},{"issue":"2014","key":"2026033014314832300_ref244","first-page":"1","article-title":"Ethereum: A secure decentralised generalised transaction ledger","volume":"151","author":"Wood","year":"2014","journal-title":"Ethereum project yellow paper"},{"key":"2026033014314832300_ref245","article-title":"Defiranger: Detecting price manipulation attacks on defi applications","author":"Wu","year":"2021","journal-title":"arXiv preprint arXiv:2104.15068"},{"issue":"3","key":"2026033014314832300_ref246","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3505263","article-title":"Time-travel investigation: Toward building a scalable attack detection framework on Ethereum","volume":"31","author":"Wu","year":"2022","journal-title":"ACM Transactions on Software Engineering and Methodology (TOSEM)"},{"key":"2026033014314832300_ref247","article-title":"DeFiRanger: Detecting DeFi Price Manipulation Attacks","author":"Wu","year":"2023","journal-title":"IEEE Transactions on Dependable and Secure Computing"},{"key":"2026033014314832300_ref248","doi-asserted-by":"publisher","first-page":"1398","DOI":"10.1145\/3368089.3417064","volume-title":"ESEC\/FSE \u201920: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Virtual Event, USA, November 8-13, 2020","author":"W\u00fcstholz","year":"2020"},{"key":"2026033014314832300_ref249","first-page":"240","volume-title":"2024 IEEE Symposium on Security and Privacy (SP)","author":"Xi","year":"2024"},{"key":"2026033014314832300_ref250","unstructured":"Xscope\n            \n          . (2022). \u201cResults: Xscope: Hunting for Cross-Chain Bridge Attacks\u201d. url: https:\/\/github.com\/Xscope-Tool\/Results?tab=readme-ov-file."},{"key":"2026033014314832300_ref251","first-page":"1029","article-title":"Cross-contract static analysis for detecting practical reentrancy vulnerabilities in smart contracts","author":"Xue","year":"2020","journal-title":"Proceedings of the 35th IEEE\/ACM International Conference on Automated Software Engineering"},{"key":"2026033014314832300_ref252","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1145\/1993498.1993532","article-title":"Finding and understanding bugs in C compilers","author":"Yang","year":"2011","journal-title":"Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation"},{"key":"2026033014314832300_ref253","first-page":"349","article-title":"Finding consensus bugs in ethereum via multi-transaction differential fuzzing","author":"Yang","year":"2021","journal-title":"15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21)"},{"key":"2026033014314832300_ref254","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/IWBOSE.2019.8666514","volume-title":"2019 IEEE International Workshop on Blockchain Oriented Software Engineering (IWBOSE)","author":"Yoo","year":"2019"},{"key":"2026033014314832300_ref255","first-page":"1","article-title":"Xscope: Hunting for cross-chain bridge attacks","author":"Zhang","year":"2022","journal-title":"Proceedings of the 37th IEEE\/ACM International Conference on Automated Software Engineering"},{"key":"2026033014314832300_ref256","article-title":"SoK: Security of Cross-chain Bridges: Attack Surfaces, Defenses, and Open Problems","author":"Zhang","year":"2023","journal-title":"arXiv preprint arXiv:2312.12573"},{"key":"2026033014314832300_ref257","first-page":"2775","article-title":"{TXSPECTOR}: Uncovering attacks in ethereum from transactions","author":"Zhang","year":"2020","journal-title":"29th USENIX Security Symposium (USENIX Security 20)"},{"key":"2026033014314832300_ref258","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/978-3-030-50029-0_21","volume-title":"Coordination Models and Languages: 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15\u201319, 2020, Proceedings 22","author":"Zhang","year":"2020"},{"key":"2026033014314832300_ref259","first-page":"1757","article-title":"Your exploit is mine: instantly synthesizing counterattack smart contract","author":"Zhang","year":"2023","journal-title":"32nd USENIX Security Symposium (USENIX Security 23)"},{"key":"2026033014314832300_ref260","doi-asserted-by":"publisher","first-page":"615","DOI":"10.1109\/ICSE48619.2023.00061","volume-title":"45th IEEE\/ACM International Conference on Software Engineering, ICSE 2023, Melbourne, Australia, May 14-20, 2023","author":"Zhang","year":"2023"},{"key":"2026033014314832300_ref261","doi-asserted-by":"publisher","first-page":"2444","DOI":"10.1109\/SP46215.2023.10179435","volume-title":"44th IEEE Symposium on Security and Privacy, SP 2023, San Francisco, CA, USA, May 21-25, 2023","author":"Zhou","year":"2023"}],"container-title":["Foundations and Trends\u00ae in Privacy and Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/ftsec\/article-pdf\/8\/1\/1\/11156241\/3300000044en.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/www.emerald.com\/ftsec\/article-pdf\/8\/1\/1\/11156241\/3300000044en.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T18:53:12Z","timestamp":1777488792000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.emerald.com\/ftsec\/article\/8\/1\/1\/1332468\/Security-Analysis-and-Formal-Verification-on"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,30]]},"references-count":261,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,6,30]]}},"URL":"https:\/\/doi.org\/10.1561\/3300000044","relation":{},"ISSN":["2474-1558","2474-1566"],"issn-type":[{"value":"2474-1558","type":"print"},{"value":"2474-1566","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,30]]}}}