{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T07:32:22Z","timestamp":1775633542100,"version":"3.50.1"},"reference-count":69,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"6","license":[{"start":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T00:00:00Z","timestamp":1761955200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T00:00:00Z","timestamp":1761955200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T00:00:00Z","timestamp":1761955200000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"Singapore Ministry of Education Academic Research Fund Tier 2","award":["T2EP20224-0003"],"award-info":[{"award-number":["T2EP20224-0003"]}]},{"name":"Nanyang Technological University Centre for Computational Technologies in Finance"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Dependable and Secure Comput."],"published-print":{"date-parts":[[2025,11]]},"DOI":"10.1109\/tdsc.2025.3592705","type":"journal-article","created":{"date-parts":[[2025,8,4]],"date-time":"2025-08-04T18:48:14Z","timestamp":1754333294000},"page":"7172-7188","source":"Crossref","is-referenced-by-count":3,"title":["Automated Invariant Generation for Solidity Smart Contracts"],"prefix":"10.1109","volume":"22","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6709-3721","authenticated-orcid":false,"given":"Ye","family":"Liu","sequence":"first","affiliation":[{"name":"Nanyang Technological University, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0186-9560","authenticated-orcid":false,"given":"Chengxuan","family":"Zhang","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4562-8208","authenticated-orcid":false,"given":"Yi","family":"Li","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","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":"ref2","article-title":"Binance smart chain","volume-title":"Introduction Binance Smart Chain","year":"2020"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3345664"},{"key":"ref4","article-title":"Overflow attack in ethereum smart contracts","year":"2020"},{"key":"ref5","article-title":"Bancor\u2019s bug exposes dangerously common practice in ethereum DeFi","author":"Shevchenko","year":"2020"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1049\/sfw2.12056"},{"key":"ref7","article-title":"EIP-20: A standard interface for tokens","year":"2015"},{"key":"ref8","article-title":"An incompatibility in ethereum smart contract threatening dApp ecosystem","author":"Guo","year":"2018"},{"key":"ref9","article-title":"Ethereum tokens worth 1b vulnerable to \u2018Fake Deposit Attack\u2019","author":"Hui","year":"2020"},{"key":"ref10","article-title":"OpenZeppelin","volume-title":"openZeppelin Contracts","year":"2022"},{"key":"ref11","article-title":"Inconsistency between the code and the doc of VestingWallet.release","year":"2022"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3556963"},{"key":"ref13","article-title":"Daikon","volume-title":"Daikon Invariant Detect.","year":"2021"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2020.3037332"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385982"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/3498665"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00032"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-41600-3_11"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3559539"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/3551349.3556962"},{"key":"ref22","article-title":"Openzeppelin erc20 contract specifications","year":"2023"},{"key":"ref23","article-title":"Openzeppelin erc721 contract specifications","year":"2023"},{"key":"ref24","article-title":"ERC20-K: Formal executable specification of ERC20","author":"Rou","year":"2023"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2004.22"},{"key":"ref26","article-title":"Esc\/Java user\u2019s manual","volume":"2000","author":"Leino","year":"2000","journal-title":"ESC"},{"issue":"131","key":"ref27","first-page":"1","article-title":"This is Boogie 2","volume":"178","author":"Leino","year":"2008","journal-title":"Manuscript KRML"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/605466.605469"},{"key":"ref29","article-title":"Formal specification and verification of smart contracts for azure blockchain","author":"Wang","year":"2018"},{"key":"ref30","article-title":"Solidity source analyzer","year":"2021"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-NIER.2019.00009"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/SANER64311.2025.00022"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"ref34","article-title":"Z3","author":"Research","year":"2022"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00022"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/BIGCOM.2019.00021"},{"key":"ref37","article-title":"Ethereum in BigQuery: A public dataset for smart contract analytics","author":"ETL","year":"2017"},{"key":"ref38","article-title":"Securing web3 with decentralized intelligence","year":"2023"},{"key":"ref39","article-title":"Openzeppelin pausable contract specifications","year":"2023"},{"key":"ref40","article-title":"ERC 20 - OpenZeppelin docs","year":"2023"},{"key":"ref41","article-title":"ERC 721 - OpenZeppelin docs","year":"2023"},{"key":"ref42","article-title":"Gambit: Mutant generation for solidity","year":"2022"},{"key":"ref43","article-title":"sec-bit\/awesome-buggy-erc20-tokens: A collection of vulnerabilities in ERC20 smart contracts with tokens affected","author":"Labs","year":"2018"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/SP54263.2024.00126"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2025.241357"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/3540250.3558923"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/3660786"},{"key":"ref48","article-title":"Understanding the DAO attack","author":"Siegel","year":"2016"},{"key":"ref49","article-title":"The parity wallet hack explained","author":"Santiago","year":"2017"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1109\/WETSEB.2019.00008"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385990"},{"key":"ref52","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1145\/3194113.3194115","article-title":"Smartcheck: Static analysis of ethereum smart contracts","volume-title":"Proc. 1st Int. Workshop Emerg. Trends Softw. Eng. Blockchain","author":"Tikhomirov","year":"2018"},{"key":"ref53","article-title":"Software reliability lab","year":"2019"},{"key":"ref54","article-title":"Precise attack synthesis for smart contracts","author":"Feng","year":"2019"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"ref56","article-title":"Symbolic execution tool for smart contracts","year":"2019"},{"key":"ref57","volume-title":"A Secur. Anal. Tool for EVM Bytecode","year":"2019"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2018.23082"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238177"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1145\/3368089.3417064"},{"key":"ref61","article-title":"Trail of bits","year":"2019"},{"key":"ref62","article-title":"An analysis tool for smart contracts","year":"2019"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00024"},{"key":"ref64","doi-asserted-by":"crossref","first-page":"778","DOI":"10.1145\/3377811.3380334","article-title":"Sfuzz: An efficient adaptive fuzzer for solidity smart contracts","volume-title":"Proc. ACM\/IEEE 42nd Int. Conf. Softw. Eng.","author":"Nguyen","year":"2020"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534372"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00061"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1145\/3597503.3639128"},{"key":"ref68","article-title":"3 hacks an audit could not find","year":"2023"},{"key":"ref69","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"}],"container-title":["IEEE Transactions on Dependable and Secure Computing"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/8858\/11242243\/11107291.pdf?arnumber=11107291","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,14]],"date-time":"2025-11-14T21:00:50Z","timestamp":1763154050000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11107291\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11]]},"references-count":69,"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.1109\/tdsc.2025.3592705","relation":{},"ISSN":["1545-5971","1941-0018","2160-9209"],"issn-type":[{"value":"1545-5971","type":"print"},{"value":"1941-0018","type":"electronic"},{"value":"2160-9209","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11]]}}}