{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T10:06:12Z","timestamp":1771668372227,"version":"3.50.1"},"reference-count":0,"publisher":"Slovenian Association Informatika","issue":"6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IJCAI"],"abstract":"<jats:p>Smart contracts are self-executing programs deployed on blockchain platforms that facilitateautomated and decentralized transactions. However, once deployed, they become immutable, makingthem vulnerable to catastrophic exploits, such as reentrancy, access control misconfiguration, integeroverflow, and front-running. The need for proof and verification is urgent, as evidenced by other highprofile,capital-draining incidents, such as the DAO attack and Parity wallet vulnerabilities. Abstract:We present ContractFuzzer, a systematic fuzzer for detecting vulnerabilities in Ethereum smartcontracts. Existing tools are based on static analysis, symbolic execution, or heuristic detection, andthus typically impose high false positives, low completeness, and limited formal verification. In thispaper, we introduce SmartScan, a formal verification framework that systematically checks smartcontract security by integrating FSM modeling and CTL-based model checking in nuXmv. Ourmethodology performs automatic parsing of Solidity code, automated generation of FSM and BIPmodels, conversion to the SMV format, and verification of CTL security properties. It responds todetected violations with automated counterexample generation to assist in debugging and iterative reverification.For validation, SmartScan will be tested on 10 different types of Solidity contracts thataddress 14 critical vulnerabilities. Our experimental results show 95.4% detection accuracy, 3.2% falsepositive rate, and 2.8% false negative rate, with 100% verification coverage, and average verificationtime of 3\u20137 seconds for each property, outperforming state-of-the-art tools in both coverage andprecision. SmartScan: SmartScan has a wide-ranging practical utility in discovering and diagnosingvulnerabilities such as reentrancy and access control issues, which it has been applied in, such as in acase study of a DeFi Lending contract. SmartScan provides a scalable, precise, and developer-centricapproach to improve the confidence and reliability of blockchain applications by combining exhaustiveformal verification of smart contracts with automated counterexample generation.<\/jats:p>","DOI":"10.31449\/inf.v50i6.8593","type":"journal-article","created":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T09:24:42Z","timestamp":1771665882000},"source":"Crossref","is-referenced-by-count":0,"title":["SmartScan: A Finite State Machine and CTL-Based Formal Verification Framework for Enhanced Security in Smart Contracts"],"prefix":"10.31449","volume":"50","author":[{"given":"G.","family":"Sowmya","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R.","family":"Sridevi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"16141","published-online":{"date-parts":[[2026,2,21]]},"container-title":["Informatica"],"original-title":[],"link":[{"URL":"https:\/\/www.informatica.si\/index.php\/informatica\/article\/download\/8593\/6450","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.informatica.si\/index.php\/informatica\/article\/download\/8593\/6450","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T09:24:42Z","timestamp":1771665882000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.informatica.si\/index.php\/informatica\/article\/view\/8593"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,2,21]]},"references-count":0,"journal-issue":{"issue":"6","published-online":{"date-parts":[[2026,2,21]]}},"URL":"https:\/\/doi.org\/10.31449\/inf.v50i6.8593","relation":{},"ISSN":["1854-3871","0350-5596"],"issn-type":[{"value":"1854-3871","type":"electronic"},{"value":"0350-5596","type":"print"}],"subject":[],"published":{"date-parts":[[2026,2,21]]}}}