{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T22:44:06Z","timestamp":1771022646813,"version":"3.50.1"},"reference-count":47,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2020]]},"DOI":"10.1109\/access.2020.2969437","type":"journal-article","created":{"date-parts":[[2020,2,2]],"date-time":"2020-02-02T05:44:21Z","timestamp":1580622261000},"page":"21411-21436","source":"Crossref","is-referenced-by-count":25,"title":["A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-Based Service Smart Contracts"],"prefix":"10.1109","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0165-0000","authenticated-orcid":false,"given":"Zheng","family":"Yang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7736-2251","authenticated-orcid":false,"given":"Hang","family":"Lei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4343-7803","authenticated-orcid":false,"given":"Weizhong","family":"Qian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","author":"duff","year":"1988","journal-title":"Message To The Comp Lang C Usenet Group"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2018.2880692"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2019.2905428"},{"key":"ref31","article-title":"Lolisa: Formal syntax and semantics for a subset of the solidity programming language","author":"yang","year":"2018","journal-title":"arXiv 1803 09885"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.23940\/ijpe.18.08.p9.17261734"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35746-6_3"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/11812289_4"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/640128.604150"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1145\/2699407"},{"key":"ref10","author":"rizzo","year":"2016","journal-title":"formal verification push Ethereum seeks smart contract certainty"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59451-5_2"},{"key":"ref11","article-title":"A General Formal Memory Framework in Coq for Verifying the Properties of Programs Based on Higher-Order Logic Theorem Proving with Increased Automation, Consistency, and Reusability","author":"yang","year":"2018","journal-title":"arXiv 1803 00403"},{"key":"ref12","author":"hildenbrandt","year":"2017","journal-title":"KEVM A complete semantics of the Ethereum virtual machine"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70278-0_33"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89722-6_10"},{"key":"ref15","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1145\/3167084","article-title":"Towards verifying Ethereum smart contract bytecode in Isabelle\/HOL","author":"amani","year":"2018","journal-title":"Proc 7th ACM SIGPLAN Int Conf Certified Programs Proofs (CPP)"},{"key":"ref16","article-title":"A survey of symbolic execution techniques","author":"baldoni","year":"2016","journal-title":"arXiv 1610 00502"},{"key":"ref17","article-title":"Scilla: A smart contract intermediate-level language","author":"sergey","year":"2018","journal-title":"arXiv 1801 00687"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/3139337.3139340"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993611"},{"key":"ref28","first-page":"209","article-title":"KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs","author":"cadar","year":"2008","journal-title":"Proc USENIX Symp Operat Syst Des Implement"},{"key":"ref4","year":"2017","journal-title":"Ethereum solidity documentation"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89330-1_22"},{"key":"ref3","author":"wilkinson","year":"2016","journal-title":"Storj A Peer-to-Peer Cloud Storage Network"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"ref29","author":"team","year":"2018","journal-title":"The Coq Proof Assistant Reference Manual"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45472-1_24"},{"key":"ref8","author":"alois","year":"2017","journal-title":"Ethereum Parity Hack May Impact ETH 500 000 or $146 Million"},{"key":"ref7","author":"del castillo","year":"2016","journal-title":"The DAO Attacked Code Issue Leads to $60 Million Ether Theft"},{"key":"ref2","first-page":"22","author":"narayanan","year":"2016","journal-title":"Bitcoin and Cryptocurrency Technologies A Comprehensive Introduction"},{"key":"ref9","author":"reitwiessner","year":"2016","journal-title":"Dev update Formal methods"},{"key":"ref1","author":"nakamoto","year":"2008","journal-title":"Bitcoin A Peer-to-Peer Electronic Cash System"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"ref20","author":"norrish","year":"1998","journal-title":"C Formalised in HOL"},{"key":"ref45","article-title":"Formal verification for ethereum smart contract using COQ","volume":"14","author":"yang","year":"2018","journal-title":"Int J Perform Eng"},{"key":"ref22","first-page":"1","article-title":"Verified Software Toolchain","volume":"2011","author":"appel","year":"0","journal-title":"Programming Languages and Systems"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"ref21","author":"leroy","year":"2018","journal-title":"The CompCert C Verified Compiler Documentation and User’s Manual"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.06.043"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49059-0_14"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676975"},{"key":"ref44","first-page":"60","article-title":"HOL light: An overview","author":"harrison","year":"2010","journal-title":"Theorem Proving in Higher Order Logics"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48737-9_3"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1023\/A:1015761529444"},{"key":"ref25","first-page":"132","article-title":"Featherweight Java: A minimal core calculus for java and GJ","author":"igarashi","year":"1999","journal-title":"Proc 14th ACM SIGPLAN Conf Object-Oriented Program Syst Lang Appl (OOPSLA)"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6287639\/8948470\/08970279.pdf?arnumber=8970279","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,17]],"date-time":"2021-12-17T19:51:11Z","timestamp":1639770671000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8970279\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"references-count":47,"URL":"https:\/\/doi.org\/10.1109\/access.2020.2969437","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]}}}