{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,25]],"date-time":"2026-01-25T01:00:08Z","timestamp":1769302808208,"version":"3.49.0"},"reference-count":32,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/OAPA.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2019]]},"DOI":"10.1109\/access.2019.2905428","type":"journal-article","created":{"date-parts":[[2019,3,15]],"date-time":"2019-03-15T23:15:05Z","timestamp":1552691705000},"page":"37770-37791","source":"Crossref","is-referenced-by-count":32,"title":["FEther: An Extensible Definitional Interpreter for Smart-Contract Verifications in Coq"],"prefix":"10.1109","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0165-0000","authenticated-orcid":false,"given":"Zheng","family":"Yang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hang","family":"Lei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref32","author":"sergey","year":"2018","journal-title":"Scilla a smart contract intermediate-level language"},{"key":"ref31","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"},{"key":"ref30","year":"2018","journal-title":"EOS Blockchain Platform"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1976.27"},{"key":"ref11","first-page":"387","article-title":"From hoare logic to matching logic reachability","volume":"7436","author":"ro?u","year":"2018","journal-title":"Proc Int Symp Formal Methods"},{"key":"ref12","year":"2018","journal-title":"The Coq Proof Assistant Reference Manual"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2699407"},{"key":"ref14","author":"yang","year":"2018","journal-title":"Lolisa Formal Syntax and Semantics for a Subset of the Solidity Programming Language"},{"key":"ref15","author":"wood","year":"2018","journal-title":"Ethereum A Secure Decentralised Generalised Transaction Ledger"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70278-0_33"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00022"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1023\/A:1015761529444"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/138873.138874"},{"key":"ref4","year":"2017","journal-title":"Ethereum Parity Hack May Impact ETH 500 000 or $146 Million"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03153-3_2"},{"key":"ref3","year":"2016","journal-title":"The DAO Attacked Code Issue Leads to $60 Million Ether Theft"},{"key":"ref6","author":"yang","year":"2018","journal-title":"A General Formal Memory Framework in Coq for Verifying the Properties of Programs Based on Higher-Order Logic Theorem Proving With Increased"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.07.020"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"ref8","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 OSDI"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.23940\/ijpe.18.08.p9.17261734"},{"key":"ref2","year":"2018","journal-title":"Ethereum solidity documentation"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"ref1","author":"nakamoto","year":"2008","journal-title":"Bitcoin A Peer-to-Peer Electronic Cash System"},{"key":"ref20","year":"2018","journal-title":"Mythril Documentation and User’s Manual"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.21236\/ADA360973"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/640128.604150"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2018.2880692"},{"key":"ref23","first-page":"561","article-title":"Semantics of typed lambda-calculus with constructors","author":"barbara","year":"2011","journal-title":"Logical Methods in Computer Science"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/3139337.3139340"},{"key":"ref25","year":"2018","journal-title":"The CompCert C Verified Compiler Documentation and User’s Manual"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6287639\/8600701\/08667810.pdf?arnumber=8667810","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,13]],"date-time":"2022-09-13T21:57:19Z","timestamp":1663106239000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8667810\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"references-count":32,"URL":"https:\/\/doi.org\/10.1109\/access.2019.2905428","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]}}}