{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:14:19Z","timestamp":1775873659826,"version":"3.50.1"},"reference-count":63,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"4","license":[{"start":{"date-parts":[[2023,7,1]],"date-time":"2023-07-01T00:00:00Z","timestamp":1688169600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2023,7,1]],"date-time":"2023-07-01T00:00:00Z","timestamp":1688169600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,7,1]],"date-time":"2023-07-01T00:00:00Z","timestamp":1688169600000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Dependable and Secure Comput."],"published-print":{"date-parts":[[2023,7,1]]},"DOI":"10.1109\/tdsc.2022.3200840","type":"journal-article","created":{"date-parts":[[2022,8,22]],"date-time":"2022-08-22T19:51:33Z","timestamp":1661197893000},"page":"3110-3127","source":"Crossref","is-referenced-by-count":23,"title":["Correct-by-Design Interacting Smart Contracts and a Systematic Approach for Verifying ERC20 and ERC721 Contracts With VeriSolid"],"prefix":"10.1109","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7652-2831","authenticated-orcid":false,"given":"Keerthi","family":"Nelaturu","sequence":"first","affiliation":[{"name":"Electrical and Computer Engineering, University of Toronto, Toronto, ON, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anastasia","family":"Mavridou","sequence":"additional","affiliation":[{"name":"Robust Software Engineering, Moffett Field, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emmanouela","family":"Stachtiari","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Geneva, Geneva, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Veneris","sequence":"additional","affiliation":[{"name":"Electrical and Computer Engineering, University of Toronto, Toronto, ON, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7400-2357","authenticated-orcid":false,"given":"Aron","family":"Laszka","sequence":"additional","affiliation":[{"name":"Computer Science, University of Houston, Houston, TX, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","article-title":"A ${\\$}$$50 million hack just showed that the DAO was all too human","author":"Finley","year":"2016"},{"key":"ref2","article-title":"Security news this week: ${\\$}$$280m worth of Ethereum is trapped thanks to a dumb bug","author":"Newman","year":"2017"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/MNET.001.1900656"},{"key":"ref4","article-title":"Ethereum: A secure decentralised generalised transaction ledger","author":"Wood","year":"2014"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32101-7_27"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"ref7","article-title":"Etherscan","year":"2020"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/bfb0025774"},{"key":"ref9","article-title":"Appendix of correct-by-design interacting smart contracts and a systematic approach for verifying ERC20 and ERC721 contracts with VeriSolid","author":"Nelaturu"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2011.27"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24953-7_25"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450228-5\/50013-8"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-15317-9_18"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-58387-6_28"},{"key":"ref15","article-title":"Blind auction","year":"2018"},{"key":"ref16","article-title":"Common patterns","year":"2018"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54848-2_1"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57666-4_16"},{"key":"ref19","first-page":"14","article-title":"A structural approach to operational semantics","author":"Plotkin","year":"1981"},{"key":"ref20","article-title":"Blockchain basics","year":"2019"},{"key":"ref22","article-title":"Ethereum improvement proposals","author":"Becze","year":"2020"},{"key":"ref23","article-title":"ERC-20: Token standard","author":"Vogelsteller","year":"2020"},{"key":"ref24","article-title":"ERC-721:non fungible token standard","author":"Entriken","year":"2020"},{"key":"ref25","article-title":"RFC2119","author":"Bradner","year":"2020"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/3377644.3377650"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/ICECCS51672.2020.00022"},{"key":"ref28","article-title":"Safemath library","year":"2020"},{"key":"ref29","article-title":"ERC-1155 multi-token standard","author":"Radomski","year":"2020"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1145\/3243734.3243780"},{"key":"ref34","article-title":"Manticore: Symbolic execution for humans","year":"2018"},{"key":"ref35","first-page":"54","article-title":"Smashing Ethereum smart contracts for fun and real profit","volume-title":"Proc. 9th Annu. HITB Secur. Conf.","author":"Mueller"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_30"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385990"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/WETSEB.2019.00008"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00032"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03427-6_28"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2018.23082"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/3274694.3274737"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23413"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238177"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380334"},{"key":"ref46","article-title":"Mutation testing for Ethereum smart contract","author":"Wu","year":"2019"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/3402450"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31500-9_19"},{"key":"ref49","article-title":"Formal verification of deed contract in Ethereum name service","author":"Hirai","year":"2016"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993611"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-58387-6_29"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00022"},{"key":"ref53","article-title":"Formal specification and verification of smart contracts for azure blockchain","author":"Lahiri","year":"2018"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-60774-0_15"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00057"},{"key":"ref56","article-title":"Babbage: A mechanical smart contract language","author":"Reitwiessner","year":"2019"},{"key":"ref57","article-title":"Bamboo: An embryonic smart contract language","author":"Hirai","year":"2019"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-C.2017.150"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1145\/3139337.3139340"},{"key":"ref60","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3345664"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.3390\/electronics9122042"},{"key":"ref62","article-title":"Formally verifying WebAssembly with KWasm towards an automated prover for wasm smart contracts","author":"Hjort","year":"2020"},{"key":"ref63","article-title":"Move: A language with programmable resources","author":"Blackshear","year":"2019","journal-title":"Libra Assoc."},{"key":"ref64","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/978-3-030-53288-8_7","article-title":"The move prover","volume-title":"Proc. Int. Conf. Comput. Aided Verification","author":"Zhong","year":"2020"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_8"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_1"}],"container-title":["IEEE Transactions on Dependable and Secure Computing"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8858\/10177761\/09864250.pdf?arnumber=9864250","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,12]],"date-time":"2024-01-12T00:48:55Z","timestamp":1705020535000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9864250\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,1]]},"references-count":63,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.1109\/tdsc.2022.3200840","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":[[2023,7,1]]}}}