pith. sign in

arxiv: 2512.22417 · v2 · submitted 2025-12-27 · 💻 cs.PL

Open-World Assertion Checking for Smart Contracts via Game Semantics

Vasileios Koutavas , Yu-Yang Lin , Nikos Tzevelekos This is my paper

Pith reviewed 2026-05-16 19:54 UTC · model grok-4.3

classification 💻 cs.PL
keywords game semanticssmart contractsEthereumassertion checkingYulreentrancysoundnesscompleteness
0
0 comments X

The pith

A game-semantics model supplies the first sound and complete open-world assertion checker for Ethereum smart contracts.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper introduces a framework that treats the interaction between an Ethereum smart contract and its arbitrary environment as a two-player game. The authors prove that this model is sound, meaning any assertion violation it finds corresponds to a real execution path, and complete, meaning it captures every possible open-world execution, subject to approximations in the gas model. They implement the approach in the YulTracer tool, which exhaustively searches bounded game traces on Yul code compiled from Solidity. Evaluation shows perfect detection of reentrancy vulnerabilities and correct identification of issues in the DAO and PredyPool exploits without false positives on patched versions.

Core claim

The paper establishes a two-player game semantics for modeling open interactions of Ethereum smart contracts with their environment and proves its soundness and completeness for assertion checking up to gas approximations. This semantics is realized in the YulTracer tool that performs concrete execution to explore game traces and achieves 100 percent recall and precision on reentrancy benchmarks while detecting known vulnerabilities in real-world contracts.

What carries the argument

The two-player game between the contract player and the environment player that models all possible external calls and reentrant interactions.

If this is right

  • Any assertion violation reported by the model corresponds to an actual execution that can be triggered on the blockchain.
  • The completeness guarantee ensures no possible attack is missed even when the environment behaves adversarially.
  • Fixed versions of contracts can be checked without introducing false positives.
  • The approach extends to verifying access control properties in addition to reentrancy safety.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar game models could be adapted for checking contracts on other blockchains that support similar execution models.
  • Integrating the exhaustive trace exploration into development tools might allow early detection of vulnerabilities during coding.
  • The framework opens the door to verifying more complex properties by extending the game with additional moves for different contract behaviors.

Load-bearing premise

The approximations in the gas model must accurately capture all real execution behaviors without omitting any possible interactions or introducing nonexistent ones.

What would settle it

A real Ethereum transaction sequence that causes an assertion violation not detected by YulTracer or a reported violation that does not correspond to any actual execution would disprove the soundness or completeness claims.

Figures

Figures reproduced from arXiv: 2512.22417 by Nikos Tzevelekos, Vasileios Koutavas, Yu-Yang Lin.

Figure 1
Figure 1. Figure 1: Overview of the YulToolkit processing pipeline. pair. Within the same callback, they used supply to return the same amounts back to PredyPool, this time credited to the attack pair. Because the end-of-trade checks validated global per-token balances rather than per-pair, the transaction passed. In a subsequent transaction, the attacker withdrew from their pair as if they had provided the liquidity. Callbac… view at source ↗
Figure 2
Figure 2. Figure 2: Overview of YulToolkit’s structure. address argument specifying the msg.sender of the call message; ASSERT, which halts the analysis and reports the Game Semantics trace; REVEAL_UINT and REVEAL_ADDR, which add values to the Opponent’s known-value sets (Section 5.1); EXT_FUND, directly increasing the balance of an address; PRINT, PRINT_signed, PRINT_hex, etc. which output values to the terminal. 5 Game Sema… view at source ↗
read the original abstract

We present a game semantics framework for open-world safety analysis of Ethereum smart contracts. We model the interaction between a contract and its environment as a two-player game between the contract and the environment, and prove up to gas model approximations soundness: every assertion violation found corresponds to a real execution; and completeness: every open-world execution is captured. To our knowledge, this provides the first formal open-world interaction semantics for Ethereum smart contracts with mathematical guarantees of soundness and completeness. We implement this framework in YulTracer, an assertion reachability tool for real-world Solidity contracts, built on Yul, the intermediate language of the Solidity compiler. YulTracer uses concrete execution and exhaustively explores game traces within user-specified bounds. We evaluate it on reentrancy benchmarks, where YulTracer achieves 100% recall and precision -- the only tool to do so from those we examined -- and on two large real-world exploits (the DAO and PredyPool), where it detects the known vulnerabilities and produces no false positives on fixed versions. To our knowledge, YulTracer is the first tool to achieve this level of precision on real-world contracts without false positives. We additionally demonstrate generality of the approach via the examination of access control benchmarks.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper presents a game semantics framework for open-world safety analysis of Ethereum smart contracts, modeling contract-environment interactions as a two-player game and proving soundness (every found assertion violation is realizable) and completeness (every open-world execution is captured) up to gas model approximations. It implements the approach in YulTracer, a tool for assertion reachability in Yul/Solidity contracts that exhaustively explores bounded game traces via concrete execution, and evaluates it on reentrancy benchmarks (achieving 100% recall and precision) plus real-world exploits (DAO and PredyPool) where it detects known vulnerabilities with no false positives on fixed versions.

Significance. If the soundness and completeness results hold under a faithful gas approximation, the work would establish the first formal open-world interaction semantics for Ethereum contracts with mathematical guarantees, addressing a key gap in smart contract verification. The practical tool achieving perfect precision on benchmarks and real exploits, plus generality on access control, would represent a notable advance over existing analyzers.

major comments (2)
  1. [Framework and soundness/completeness section] The soundness and completeness theorems (stated in the abstract and developed in the framework section) are explicitly qualified as holding only 'up to gas model approximations', yet no concrete gas rules, deviations from the EVM yellow paper, or preservation argument for assertion reachability under the approximation are provided. This is load-bearing for the central claims, as gas-dependent control flow (e.g., out-of-gas on CALL or loops) could introduce spurious violations or miss real ones.
  2. [Evaluation section] The evaluation claims 100% precision/recall on reentrancy benchmarks and no false positives on fixed real-world contracts, but without details on the exact gas model used in YulTracer or how bounds were chosen to ensure completeness within those bounds, it is difficult to assess whether the results support the theoretical guarantees.
minor comments (2)
  1. [Abstract] The repeated 'to our knowledge' phrasing for novelty claims in the abstract could be strengthened by explicit comparison to prior game-semantics applications in verification.
  2. [Framework section] Notation for game traces and player moves should be introduced with a small example early in the framework section to improve readability for readers unfamiliar with game semantics.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful and constructive review of our manuscript. The comments highlight important points about the presentation of the gas model and its connection to the evaluation. We address each major comment below and will make the indicated revisions to strengthen the paper.

read point-by-point responses

  1. Referee: [Framework and soundness/completeness section] The soundness and completeness theorems (stated in the abstract and developed in the framework section) are explicitly qualified as holding only 'up to gas model approximations', yet no concrete gas rules, deviations from the EVM yellow paper, or preservation argument for assertion reachability under the approximation are provided. This is load-bearing for the central claims, as gas-dependent control flow (e.g., out-of-gas on CALL or loops) could introduce spurious violations or miss real ones.

    Authors: We agree that the current manuscript would benefit from greater explicitness on this point. The gas approximation is designed to abstract away fine-grained EVM costs while preserving the interaction behaviors that matter for assertion reachability in the game model. In the revised version we will add a dedicated subsection that (i) states the concrete gas rules used for operations such as CALL, loops, and storage accesses, (ii) lists the principal deviations from the EVM yellow paper (primarily the imposition of explicit per-trace gas bounds to guarantee termination), and (iii) sketches a preservation argument showing that reachability of assertions is preserved under this approximation for the open-world setting. This will make the soundness and completeness statements fully rigorous relative to the stated model. revision: yes

  2. Referee: [Evaluation section] The evaluation claims 100% precision/recall on reentrancy benchmarks and no false positives on fixed real-world contracts, but without details on the exact gas model used in YulTracer or how bounds were chosen to ensure completeness within those bounds, it is difficult to assess whether the results support the theoretical guarantees.

    Authors: We will expand the evaluation section to describe the gas model actually implemented in YulTracer (which follows the approximated rules introduced in the framework) and to explain the rationale for the chosen bounds. Specifically, we will report the maximum trace depth and per-trace gas limits used for each benchmark and real-world contract, together with an argument that these bounds are sufficient to cover all relevant execution paths for the known vulnerabilities. This will demonstrate that the reported 100 % precision and recall are obtained within a model that is consistent with the theoretical guarantees. revision: yes

Circularity Check

0 steps flagged

No significant circularity; soundness and completeness proven relative to explicitly defined game model and gas approximations

full rationale

The paper defines a two-player game semantics for contract-environment interactions and states that soundness (every found violation is realizable) and completeness (every open-world execution captured) hold up to gas model approximations. No equations or steps reduce by construction to fitted inputs, self-definitions, or prior self-citations; the guarantees are explicitly qualified as model-relative rather than absolute. Evaluation on reentrancy benchmarks and real exploits provides external validation without renaming known results or smuggling ansatzes via citation. The gas approximation is presented as a limitation rather than a hidden tautology, keeping the derivation self-contained against the stated model.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on modeling contract-environment interaction as a two-player game and on gas-cost approximations; these are introduced without independent external evidence in the abstract.

axioms (1)
  • standard math Standard game semantics assumptions for modeling interactive systems as two-player games
    Invoked to represent contract and environment interactions.
invented entities (1)
  • Game traces within user-specified bounds no independent evidence
    purpose: To exhaustively explore possible contract-environment interactions for assertion checking
    Core modeling device introduced by the framework; no independent evidence provided in abstract.

pith-pipeline@v0.9.0 · 5522 in / 1205 out tokens · 27439 ms · 2026-05-16T19:54:55.338831+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

47 extracted references · 47 canonical work pages

  1. [1]

    Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. 2000. Full Abstraction for PCF.Information and Computation163, 2, 409–470. https://doi.org/10.1006/inco.2000.2930

    work page doi:10.1006/inco.2000.2930 2000

  2. [2]

    Alexey Akhunov and Moody Salem. 2018. EIP-1153: Transient Storage Opcodes. https://eips.ethereum.org/EIPS/eip-

    work page 2018

  3. [3]

    Ethereum Improvement Proposal, created 2018-06-15

    work page 2018

  4. [4]

    Arbiscan. 2024. Predy Finance Victim Contract. https://arbiscan.io/address/0x9215748657319B17fecb2b5D086A3147BF BC8613. Predy Finance contract exploited in 14 May 2024

    work page 2024

  5. [5]

    Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. 2017. A Survey of Attacks on Ethereum Smart Contracts (SoK). InPrinciples of Security and Trust. Springer, Berlin, Heidelberg, 164–186. https://doi.org/10.1007/978-3-662-54455-6_8

    work page doi:10.1007/978-3-662-54455-6_8 2017

  6. [6]

    Gbadebo Ayoade, Erick Bauman, Latifur Khan, and Kevin Hamlen. 2019. Smart Contract Defense through Bytecode Rewriting. In2019 IEEE International Conference on Blockchain (Blockchain). 384–389. https://doi.org/10.1109/Blockc hain.2019.00059

    work page doi:10.1109/blockc 2019

  7. [7]

    2023.EIP-6780: SELFDESTRUCT only in same transaction

    Guillaume Ballet, Vitalik Buterin, and Dankrad Feist. 2023.EIP-6780: SELFDESTRUCT only in same transaction. Technical Report 6780. Ethereum Improvement Proposals. https://eips.ethereum.org/EIPS/eip-6780 Standards Track: Core

    work page 2023

  8. [8]

    Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. 1999. Symbolic Model Checking without BDDs. InTools and Algorithms for the Construction and Analysis of Systems, W. Rance Cleaveland (Ed.). Springer, Berlin, Heidelberg, 193–207. https://doi.org/10.1007/3-540-49059-0_14

    work page doi:10.1007/3-540-49059-0_14 1999

  9. [9]

    Lexi Brent, Neville Grech, Sifis Lagouvardos, Bernhard Scholz, and Yannis Smaragdakis. 2020. Ethainter: A Smart Contract Security Analyzer for Composite Vulnerabilities. InProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, London UK, 454–469. https://doi.org/10.1145/3385412.3385 990

    work page doi:10.1145/3385412.3385 2020

  10. [10]

    2019.Smart Contract Reentrancy: TheDAO

    Zhongqiang Chen. 2019.Smart Contract Reentrancy: TheDAO. https://medium.com/@zhongqiangc/smart-contract- reentrancy-thedao-f2da1d25180c Published: Aug 22, 2019; Accessed: 2025-08-21

    work page 2019

  11. [11]

    Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004. A Tool for Checking ANSI-C Programs. InTools and Algorithms for the Construction and Analysis of Systems, Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Kurt Jensen, and Andreas Podelski (Eds.). Vol. 2988. Springer Berlin Heidelberg, Berlin, Heidelberg, 168–176. https: //doi.org/10.1007/978-3-540-24730-2_15

    work page doi:10.1007/978-3-540-24730-2_15 2004

  12. [12]

    ConsenSys Diligence. 2024. Mythril: Symbolic-Execution-Based Security Analysis Tool for EVM Bytecode. https: //github.com/ConsenSysDiligence/mythril. GitHub repository, release 0.24.8 :contentReference[oaicite:0]index=0

    work page 2024

  13. [13]

    Crystal Intelligence. [n. d.]. Adolescent Anarchy: Thirteen Years of Crypto Crimes Unveiled. https://crystalintellige nce.com/rohirov/2024/06/Crystal-Intelligence-Thirteen-Years-of-Crypto-Crimes-Unveiled.pdf Accessed 2 September 2025

    work page 2024

  14. [14]

    Decentralized Application Security Project (DASP). [n. d.].DASP Top 10 (2018): Decentralized Application Security Project. NCC Group. https://dasp.co/ Site credits: David Wong; Mason Hemmel

    work page 2018

  15. [15]

    DefiLlama. 2025. Ethereum - DefiLlama. https://defillama.com/chain/ethereum. Accessed: 2025-09-02

    work page 2025

  16. [16]

    2022.EIP-6049: Deprecate SELFDESTRUCT

    William Entriken. 2022.EIP-6049: Deprecate SELFDESTRUCT. Technical Report 6049. Ethereum Improvement Proposals. https://eips.ethereum.org/EIPS/eip-6049

    work page 2022

  17. [17]

    Ethereum Foundation. [n. d.].Ethereum Execution Client Specifications. https://github.com/ethereum/execution- specs/tree/3fe6514f2d9d234e760d11af883a47c1263eff51 Experiments started at this commit and incorporate later 20 Vasileios Koutavas, Yu-Yang Lin, and Nikos Tzevelekos revisions

    work page

  18. [18]

    Etherscan. 2016. The DAO Victim Contract. https://etherscan.io/address/0xBB9bc244D798123fDe783fCc1C72d3Bb8C1 89413. Main DAO contract exploited in 17 June 2016

    work page 2016

  19. [19]

    Etherscan. 2018. SpankChain Victim Contract. https://etherscan.io/address/0xf91546835f756DA0c10cFa0CDA95b1557 7b84aA7. SpankChain payment channel contract exploited in 9 October 2018

    work page 2018

  20. [20]

    Etherscan. 2020. Lendf.Me Victim Contract. https://etherscan.io/address/0x0eEe3E3828A45f7601D5F54bF49bB01d1A9 dF5ea. dForce Lendf.Me contract exploited in 19 April 2020

    work page 2020

  21. [21]

    Joel Frank, Cornelius Aschermann, and Thorsten Holz. 2020. ETHBMC: A Bounded Model Checker for Smart Contracts. InProceedings of the 29th USENIX Conference on Security Symposium (SEC’20). USENIX Association, USA, 2757–2774

    work page 2020

  22. [22]

    2020.A Benchmark Suite for Smart Contract Vulnerabilities (Gigahorse Benchmarks)

    Neville Grech. 2020.A Benchmark Suite for Smart Contract Vulnerabilities (Gigahorse Benchmarks). https://github.com /nevillegrech/gigahorse-benchmarks Forked from smartbugs. Accessed: 2025-08-21

    work page 2020

  23. [23]

    Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis. 2020. MadMax: Analyzing the out-of-Gas World of Smart Contracts.Commun. ACM63, 10 (Sept. 2020), 87–95. https://doi.org/10.114 5/3416262

    work page 2020

  24. [24]

    J. M. E. Hyland and C.-H. Luke Ong. 2000. On Full Abstraction for PCF: I, II, and III.Information and Computation163, 2 (2000), 285–408. https://doi.org/10.1006/inco.2000.2917

    work page doi:10.1006/inco.2000.2917 2000

  25. [25]

    Bo Jiang, Ye Liu, and W. K. Chan. 2018. ContractFuzzer: Fuzzing Smart Contracts for Vulnerability Detection. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (ASE ’18). ACM, New York, NY, USA, 259–269. https://doi.org/10.1145/3238147.3238177

    work page doi:10.1145/3238147.3238177 2018

  26. [26]

    Vasileios Koutavas, Yu-Yang Lin, and Nikos Tzevelekos. 2025. An Operational Semantics for Yul. InSoftware Engineering and Formal Methods. Springer, Cham, 328–346. https://doi.org/10.1007/978-3-031-77382-2_19

    work page doi:10.1007/978-3-031-77382-2_19 2025

  27. [27]

    Satpal Singh Kushwaha, Sandeep Joshi, Dilbag Singh, Manjit Kaur, and Heung-No Lee. 2022. Systematic Review of Security Vulnerabilities in Ethereum Blockchain Smart Contract.IEEE Access10 (2022), 6605–6621. https: //doi.org/10.1109/ACCESS.2021.3140091

    work page doi:10.1109/access.2021.3140091 2022

  28. [28]

    L. Lamport. 1977. Proving the Correctness of Multiprocess Programs.IEEE Transactions on Software EngineeringSE-3, 2 (March 1977), 125–143. https://doi.org/10.1109/TSE.1977.229904

    work page doi:10.1109/tse.1977.229904 1977

  29. [29]

    Ruichao Liang, Jing Chen, Ruochen Cao, Kun He, Ruiying Du, Shuhua Li, Zheng Lin, and Cong Wu. 2025. SmartShot: Hunt Hidden Vulnerabilities in Smart Contracts Using Mutable Snapshots.Proceedings of the ACM on Software Engineering2, FSE (June 2025), 65–85. https://doi.org/10.1145/3715714

    work page doi:10.1145/3715714 2025

  30. [30]

    Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, and Artem Dinaburg. 2019. Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts. InProceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering (ASE). 1186–1189. https://doi.org/10.110...

    work page doi:10.1109/ase.2019.00133 2019

  31. [31]

    Hanno Nickau. 1994. Hereditarily Sequential Functionals. InLogical Foundations of Computer Science, Third International Symposium, LFCS’94, St. Petersburg, Russia, July 11-14, 1994, Proceedings (Lecture Notes in Computer Science, Vol. 813), Anil Nerode and Yuri V. Matiyasevich (Eds.). Springer, 253–264. https://doi.org/10.1007/3-540-58140-5_25

    work page doi:10.1007/3-540-58140-5_25 1994

  32. [32]

    pcaversaccio. 2022. A Historical Collection of Reentrancy Attacks. https://github.com/pcaversaccio/reentrancy-attacks Accessed: 2025-08-21

    work page 2022

  33. [33]

    2024.Postmortem Report on the Events of May 14, 2024

    Predy Finance. 2024.Postmortem Report on the Events of May 14, 2024. https://predyfinance.medium.com/postmortem- report-on-the-details-of-the-events-of-may-14-2024-8690508c820b Published: May 16, 2024; Accessed: 2025-08-21

    work page 2024

  34. [34]

    Predy Finance. 2024. Predy V6. https://docs.predy.finance/predy-v6/. Accessed: 2025-9-8

    work page 2024

  35. [35]

    2020.How SpankChain Got Hacked—A Reentrancy Attack Explained

    Alex Roan. 2020.How SpankChain Got Hacked—A Reentrancy Attack Explained. https://medium.com/swlh/how- spankchain-got-hacked-af65b933393c Published: March 26, 2020; Accessed: 2025-08-21

    work page 2020

  36. [36]

    sirhashalot. 2023. Smart Contract Vulnerabilities (SCV) list. https://github.com/sirhashalot/SCV-List Accessed 2 September 2025

    work page 2023

  37. [37]

    2020.Details of the Lendf.Me Reentrancy Attack

    SlowMist. 2020.Details of the Lendf.Me Reentrancy Attack. https://slowmist.medium.com/slowmist-details-of-lendf- me-reentrancy-attack-3e168ab5f2b1 Published: April 19, 2020; Accessed: 2025-08-21

    work page 2020

  38. [38]

    Yannis Smaragdakis, Neville Grech, Sifis Lagouvardos, Konstantinos Triantafyllou, and Ilias Tsatiris. 2021. Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts.Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts (Artifact)5, OOPSLA (Oct. 2021), 163:1–163:30. https:...

    work page doi:10.1145/3485540 2021

  39. [39]

    2020.SmartBugs: A Framework for Analysing Ethereum Smart Contracts

    SmartBugs Team. 2020.SmartBugs: A Framework for Analysing Ethereum Smart Contracts. https://github.com/smart bugs/smartbugs Accessed: 2025-08-21

    work page 2020

  40. [40]

    Solidity Team. 2024. List of known bugs - Solidity 0.8.31 documentation. https://docs.soliditylang.org/en/develop/bug s.html Accessed 2 September 2025

    work page 2024

  41. [41]

    Solidity Team. 2024. Solidity 0.8.24 Release Announcement. https://soliditylang.org/blog/2024/01/26/solidity-0.8.24- release-announcement. Blog post, published 2024-01-26.. A Bounded Game Semantics Checker for Precise Smart Contract Analysis 21

    work page 2024

  42. [42]

    Solidity Team. 2025. Security Considerations - Solidity Documentation. https://docs.soliditylang.org/en/latest/security- considerations.html. Accessed: 2025-09-05

    work page 2025

  43. [43]

    Solidity Team. 2025. Yul: Solidity 0.8.31 Documentation. https://docs.soliditylang.org/en/latest/yul.html. Accessed: 7 September 2025

    work page 2025

  44. [44]

    Jon Stephens, Kostas Ferles, Benjamin Mariano, Shuvendu Lahiri, and Isil Dillig. 2021. SmartPulse: Automated Checking of Temporal Properties in Smart Contracts. In2021 IEEE Symposium on Security and Privacy (SP). 555–571. https://doi.org/10.1109/SP40001.2021.00085

    work page doi:10.1109/sp40001.2021.00085 2021

  45. [45]

    Uniswap. 2025. The Uniswap Protocol. https://docs.uniswap.org/concepts/uniswap-protocol. Accessed: 2025-9-8

    work page 2025

  46. [46]

    Fernando Richter Vidal, Naghmeh Ivaki, and Nuno Laranjeiro. 2024. Vulnerability Detection Techniques for Smart Contracts: A Systematic Literature Review.Journal of Systems and Software217 (Nov. 2024), 112160. https://doi.org/ 10.1016/j.jss.2024.112160

    work page doi:10.1016/j.jss.2024.112160 2024

  47. [47]

    Yuan Zhuang, Zhenguang Liu, Peng Qian, Qi Liu, Xiang Wang, and Qinming He. 2020. Smart Contract Vulnerability Detection Using Graph Neural Network. InProceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence. International Joint Conferences on Artificial Intelligence Organization, Yokohama, Japan, 3283–3290. https://doi.org...

    work page doi:10.24963/ijcai.2020/454 2020