{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T15:46:33Z","timestamp":1777131993505,"version":"3.51.4"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"7","license":[{"start":{"date-parts":[[2022,10,12]],"date-time":"2022-10-12T00:00:00Z","timestamp":1665532800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,10,12]],"date-time":"2022-10-12T00:00:00Z","timestamp":1665532800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"name":"National Key R&D Program of China under Grant","award":["No.2021YFB2700603"],"award-info":[{"award-number":["No.2021YFB2700603"]}]},{"name":"National Natural Science Foundation of China under Grant","award":["No.62172405"],"award-info":[{"award-number":["No.62172405"]}]},{"name":"National Natural Science Foundation of China under Grant","award":["No.62072487"],"award-info":[{"award-number":["No.62072487"]}]},{"name":"Beijing Natural Science Foundation under Grant","award":["No.M21036"],"award-info":[{"award-number":["No.M21036"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Empir Software Eng"],"published-print":{"date-parts":[[2022,12]]},"DOI":"10.1007\/s10664-022-10218-2","type":"journal-article","created":{"date-parts":[[2022,10,12]],"date-time":"2022-10-12T02:02:17Z","timestamp":1665540137000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["SmartFast: an accurate and robust formal analysis tool for Ethereum smart contracts"],"prefix":"10.1007","volume":"27","author":[{"given":"Zhaoxuan","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Siqi","family":"Lu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rui","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rui","family":"Xue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenqiu","family":"Ma","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rujin","family":"Liang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ziming","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sheng","family":"Gao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,10,12]]},"reference":[{"key":"10218_CR1","unstructured":"Beosin (2020) Beosin: Blockchain security one-stop service. [EB\/OL]. https:\/\/beosin.com\/#\/. Accessed 1 May 2021"},{"key":"10218_CR2","unstructured":"Blockchain C (2018) Bamboo: a morphing smart contract language. [EB\/OL]. https:\/\/github.com\/cornellblockchain\/bamboo. Accessed 1 May 2021"},{"key":"10218_CR3","doi-asserted-by":"crossref","unstructured":"Bocek T, Stiller B (2018) Smart contracts\u2013blockchains in the wings. In: Digital marketplaces unleashed. Springer, pp 169\u2013184","DOI":"10.1007\/978-3-662-49275-8_19"},{"key":"10218_CR4","doi-asserted-by":"crossref","unstructured":"Chen T, Cao R, Li T, Luo X, Gu G, Zhang Y, Liao Z, Zhu H, Chen G, He Z, Tang Y, Lin X, Zhang X (2020) SODA: a generic online detection framework for smart contracts. In: NDSS. The Internet Society","DOI":"10.14722\/ndss.2020.24449"},{"key":"10218_CR5","doi-asserted-by":"crossref","unstructured":"Choi J, Kim D, Kim S, Grieco G, Groce A, Cha S K (2021) SMARTIAN: enhancing smart contract fuzzing with static and dynamic data-flow analyses. In: ASE. IEEE, pp 227\u2013239","DOI":"10.1109\/ASE51524.2021.9678888"},{"key":"10218_CR6","unstructured":"Corporation M (2020) The z3 theorem prover. [EB\/OL]. https:\/\/github.com\/Z3Prover\/z3. Accessed 1 May 2021"},{"key":"10218_CR7","unstructured":"DappHub (2019) Formal verification of multicollateral dai in the k framework. [EB\/OL]. https:\/\/github.com\/dapphub\/k-dss\/. 1 Accessed May 2021"},{"key":"10218_CR8","doi-asserted-by":"crossref","unstructured":"Durieux T, Ferreira J F, Abreu R, Cruz P (2020) Empirical review of automated analysis tools on 47, 587 ethereum smart contracts. In: ICSE. ACM, pp 530\u2013541","DOI":"10.1145\/3377811.3380364"},{"key":"10218_CR9","unstructured":"Etherscan (2017) Contracts with verified source codes only. [EB\/OL]. https:\/\/etherscan.io\/contractsVerified. Accessed 1 May 2021"},{"key":"10218_CR10","doi-asserted-by":"crossref","unstructured":"Feist J, Grieco G, Groce A (2019) Slither: a static analysis framework for smart contracts. In: WETSEB@ICSE. IEEE\/ACM, pp 8\u201315","DOI":"10.1109\/WETSEB.2019.00008"},{"key":"10218_CR11","unstructured":"Foundation E (2020) The solidity contract-oriented programming language. [EB\/OL]. https:\/\/github.com\/ethereum\/solidity. Accessed 1 May 2021"},{"key":"10218_CR12","unstructured":"Frank J, Aschermann C, Holz T (2020) ETHBMC: a bounded model checker for smart contracts. In: USENIX Security symposium. USENIX Association, pp 2757\u20132774"},{"key":"10218_CR13","unstructured":"Grishchenko I, Maffei M, Schneidewind C (2018a) Ethertrust: sound static analysis of ethereum bytecode. Technische Universit\u00e4t Wien. Tech Rep"},{"key":"10218_CR14","doi-asserted-by":"crossref","unstructured":"Grishchenko I, Maffei M, Schneidewind C (2018b) Foundations and tools for the static analysis of ethereum smart contracts. In: CAV (1), vol 10981. Springer. Lecture Notes in Computer Science, pp 51\u201378","DOI":"10.1007\/978-3-319-96145-3_4"},{"key":"10218_CR15","doi-asserted-by":"crossref","unstructured":"Grishchenko I, Maffei M, Schneidewind C (2018c) A semantic framework for the security analysis of ethereum smart contracts. In: POST. Lecture Notes in Computer Science, vol 10804. Springer, pp 243\u2013269","DOI":"10.1007\/978-3-319-89722-6_10"},{"key":"10218_CR16","doi-asserted-by":"crossref","unstructured":"He J, Balunovic M, Ambroladze N, Tsankov P, Vechev M T (2019) Learning to fuzz from symbolic execution with application to smart contracts. In: CCS. ACM, pp 531\u2013548","DOI":"10.1145\/3319535.3363230"},{"key":"10218_CR17","doi-asserted-by":"crossref","unstructured":"Hildenbrandt E, Saxena M, Rodrigues N, Zhu X, Daian P, Guth D, Moore B M, Park D, Zhang Y, Stefanescu A, Rosu G (2018) KEVM: a complete formal semantics of the ethereum virtual machine. In: CSF. IEEE Computer Society, pp 204\u2013217","DOI":"10.1109\/CSF.2018.00022"},{"key":"10218_CR18","doi-asserted-by":"crossref","unstructured":"Jiao J, Kan S, Lin S, San\u00e1n D, Liu Y, Sun J (2020) Semantic understanding of smart contracts: Executable operational semantics of solidity. In: IEEE S&P. IEEE, pp 1695\u20131712","DOI":"10.1109\/SP40000.2020.00066"},{"key":"10218_CR19","doi-asserted-by":"crossref","unstructured":"Kalra S, Goel S, Dhawan M, Sharma S (2018) ZEUS: analyzing safety of smart contracts. In: NDSS. The Internet Society","DOI":"10.14722\/ndss.2018.23082"},{"key":"10218_CR20","unstructured":"Kasampalis T, Guth D, Moore B, Serbanuta T, Serbanuta V, Filaretti D, Rosu G, Johnson R (2018) Iele: an intermediate-level blockchain language designed and implemented using formal semantics. Tech. rep."},{"key":"10218_CR21","unstructured":"Krupp J, Rossow C (2018) Teether: gnawing at ethereum to automatically exploit smart contracts. In: USENIX security symposium. USENIX Association, pp 1317\u20131333"},{"key":"10218_CR22","doi-asserted-by":"crossref","unstructured":"Liu C, Liu H, Cao Z, Chen Z, Chen B, Roscoe B (2018) Reguard: finding reentrancy bugs in smart contracts. In: ICSE. ACM, pp 65\u201368","DOI":"10.1145\/3183440.3183495"},{"key":"10218_CR23","doi-asserted-by":"crossref","unstructured":"Lu N, Wang B, Zhang Y, Shi W, Esposito C (2019) Neucheck: a more practical ethereum smart contract security analysis tool. Softw: Pract Exp","DOI":"10.1002\/spe.2745"},{"key":"10218_CR24","doi-asserted-by":"crossref","unstructured":"Luu L, Chu D, Olickel H, Saxena P, Hobor A (2016) Making smart contracts smarter. In: CCS. ACM, pp 254\u2013269","DOI":"10.1145\/2976749.2978309"},{"key":"10218_CR25","doi-asserted-by":"crossref","unstructured":"Nguyen T D, Pham L H, Sun J, Lin Y, Minh QT (2020) sfuzz: an efficient adaptive fuzzer for solidity smart contracts. In: ICSE. ACM, pp 778\u2013788","DOI":"10.1145\/3377811.3380334"},{"key":"10218_CR26","unstructured":"Nipkow T, Paulson L C, Wenzel M (2283) Isabelle\/HOL\u2014a proof assistant for higher-order logic. In: Lecture Notes in Computer Science. Springer"},{"key":"10218_CR27","doi-asserted-by":"crossref","unstructured":"Permenev A, Dimitrov D, Tsankov P, Drachsler-Cohen D, Vechev MT (2020) Verx: safety verification of smart contracts. In: IEEE symposium on security and privacy. IEEE, pp 1661\u20131677","DOI":"10.1109\/SP40000.2020.00024"},{"key":"10218_CR28","unstructured":"Reis J S, Crocker P A, de Sousa S M (2020) Tezla, an intermediate representation for static analysis of michelson smart contracts. In: FMBC@CAV, Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, OASIcs, vol 84, pp 4:1\u20134:12"},{"key":"10218_CR29","doi-asserted-by":"crossref","unstructured":"Rodler M, Li W, Karame G O, Davi L (2019) Sereum: protecting existing smart contracts against re-entrancy attacks. In: NDSS. The Internet Society","DOI":"10.14722\/ndss.2019.23413"},{"key":"10218_CR30","doi-asserted-by":"crossref","unstructured":"Schneidewind C, Grishchenko I, Scherer M, Maffei M (2020) Ethor: practical and provably sound static analysis of ethereum smart contracts. In: CCS. ACM, pp 621\u2013640","DOI":"10.1145\/3372297.3417250"},{"key":"10218_CR31","doi-asserted-by":"crossref","unstructured":"Sergey I, Hobor A (2017) A concurrent perspective on smart contracts. In: Financial cryptography workshops. Lecture Notes In Computer Science, vol 10323. Springer, pp 478\u2013493","DOI":"10.1007\/978-3-319-70278-0_30"},{"key":"10218_CR32","unstructured":"Sergey I, Kumar A, Hobor A (2018) Scilla: a smart contract intermediate-level language. CoRR. arXiv:1801.00687"},{"key":"10218_CR33","unstructured":"Software C (2020) Security analysis tool for evm bytecode. [EB\/OL]. https:\/\/github.com\/ConsenSys\/mythril. Accessed 1 May 2021"},{"key":"10218_CR34","unstructured":"Solidity (2020) Solidity v0.5.0 breaking changes. [EB\/OL]. https:\/\/docs.soliditylang.org\/en\/v0.5.0\/050-breaking-changes.html. Accessed 1 May 2021"},{"key":"10218_CR35","unstructured":"SRI Lab E Z (2020) Securify v2.0. [EB\/OL]. https:\/\/github.com\/eth-sri\/securify2. Accessed 1 May 2021"},{"key":"10218_CR36","unstructured":"Team V (2020) Vyper documentation. [EB\/OL]. https:\/\/vyper.readthedocs.io\/en\/latest\/. Accessed 1 May 2021"},{"key":"10218_CR37","unstructured":"Tezos (2020) Michelson: the language of smart contracts in dune. [EB\/OL]. https:\/\/www.liquidity-lang.org\/doc\/reference\/michelson.html. Accessed 1 May 2021"},{"key":"10218_CR38","doi-asserted-by":"crossref","unstructured":"Tikhomirov S, Voskresenskaya E, Ivanitskiy I, Takhaviev R, Marchenko E, Alexandrov Y (2018) Smartcheck: static analysis of ethereum smart contracts. In: WETSEB@ICSE. ACM, pp 9\u201316","DOI":"10.1145\/3194113.3194115"},{"key":"10218_CR39","doi-asserted-by":"crossref","unstructured":"Torres C F, Sch\u00fctte J, State R (2018) Osiris: hunting for integer bugs in ethereum smart contracts. In: ACSAC. ACM, pp 664\u2013676","DOI":"10.1145\/3274694.3274737"},{"key":"10218_CR40","doi-asserted-by":"crossref","unstructured":"Tsankov P, Dan A M, Drachsler-Cohen D, Gervais A, B\u00fcnzli F, Vechev M T (2018) Securify: practical security analysis of smart contracts. In: CCS. ACM, pp 67\u201382","DOI":"10.1145\/3243734.3243780"},{"issue":"2014","key":"10218_CR41","first-page":"1","volume":"151","author":"G Wood","year":"2014","unstructured":"Wood G, et al. (2014) Ethereum: a secure decentralised generalised transaction ledger. Ethereum Project Yellow Paper 151(2014):1\u201332","journal-title":"Ethereum Project Yellow Paper"}],"container-title":["Empirical Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-022-10218-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10664-022-10218-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-022-10218-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,21]],"date-time":"2022-11-21T02:22:43Z","timestamp":1668997363000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10664-022-10218-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,12]]},"references-count":41,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2022,12]]}},"alternative-id":["10218"],"URL":"https:\/\/doi.org\/10.1007\/s10664-022-10218-2","relation":{},"ISSN":["1382-3256","1573-7616"],"issn-type":[{"value":"1382-3256","type":"print"},{"value":"1573-7616","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,12]]},"assertion":[{"value":"29 July 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 October 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare that they have no known competing financial interests or personal relationships that could have appeared to influence the work reported in this paper","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"<!--Emphasis Type='Bold' removed-->Conflict of Interest"}}],"article-number":"197"}}