{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:03Z","timestamp":1750220643838,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":11,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,20]],"date-time":"2020-10-20T00:00:00Z","timestamp":1603152000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,10,20]]},"DOI":"10.1145\/3424978.3425032","type":"proceedings-article","created":{"date-parts":[[2020,10,15]],"date-time":"2020-10-15T19:09:24Z","timestamp":1602788964000},"page":"1-8","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Resolution for Scalability Problem of Record Datatype Based Formal Memory Models in Coq"],"prefix":"10.1145","author":[{"given":"Zheng","family":"Yang","sequence":"first","affiliation":[{"name":"School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hang","family":"Lei","sequence":"additional","affiliation":[{"name":"School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weizhong","family":"Qian","sequence":"additional","affiliation":[{"name":"School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zehui","family":"Yan","sequence":"additional","affiliation":[{"name":"School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Weiru","family":"Zeng","sequence":"additional","affiliation":[{"name":"School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,10,20]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"A Peer-to-Peer Electronic Cash System","author":"Nakamoto S","year":"2008","unstructured":"S Nakamoto ( 2008 ). Bitcoin , A Peer-to-Peer Electronic Cash System , http:\/\/usebitcoins.info\/index.php\/bitcoin-a-peer-to-peer-electronic-cash-system. S Nakamoto (2008). Bitcoin, A Peer-to-Peer Electronic Cash System, http:\/\/usebitcoins.info\/index.php\/bitcoin-a-peer-to-peer-electronic-cash-system."},{"volume-title":"The Coq Proof Assistant Reference Manual, https:\/\/coq.inria.fr\/distrib\/current\/refman\/","year":"2020","key":"e_1_3_2_1_2_1","unstructured":"Coq Development Team ( 2020 ). The Coq Proof Assistant Reference Manual, https:\/\/coq.inria.fr\/distrib\/current\/refman\/ . Coq Development Team (2020). The Coq Proof Assistant Reference Manual, https:\/\/coq.inria.fr\/distrib\/current\/refman\/."},{"key":"e_1_3_2_1_3_1","volume-title":"L C Paulson and M Wenzel","author":"Nipkow T","year":"2002","unstructured":"T Nipkow , L C Paulson and M Wenzel ( 2002 ). Isabelle\/HOL: a proof assistant for higher-order logic. Springer Science & Business Media . Vol. 2283 . T Nipkow, L C Paulson and M Wenzel (2002). Isabelle\/HOL: a proof assistant for higher-order logic. Springer Science & Business Media. Vol. 2283."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_3_2_1_5_1","first-page":"37770","volume-title":"FEther: An Extensible Definitional Interpreter for Smart-Contract Verifications in Coq","author":"Yang Z","year":"2019","unstructured":"Z Yang and H Lei ( 2019 ). FEther: An Extensible Definitional Interpreter for Smart-Contract Verifications in Coq . 2019, IEEE Access , vol. 7 , pp. 37770 -- 37791 , doi: 10.1109\/ACCESS. 2905428. 10.1109\/ACCESS Z Yang and H Lei (2019). FEther: An Extensible Definitional Interpreter for Smart-Contract Verifications in Coq. 2019, IEEE Access, vol. 7, pp. 37770--37791, doi: 10.1109\/ACCESS. 2905428."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676975"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.06.043"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.23940\/ijpe.19.11.p19.29983007"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1002\/cpe.4061"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.23940\/ijpe.18.08.p9.17261734"},{"key":"e_1_3_2_1_11_1","volume-title":"The EOS Reference Manual, https:\/\/eos.io\/","author":"Development Team EOS","year":"2020","unstructured":"EOS Development Team ( 2020 ). The EOS Reference Manual, https:\/\/eos.io\/ . EOS Development Team (2020). The EOS Reference Manual, https:\/\/eos.io\/."}],"event":{"name":"CSAE 2020: The 4th International Conference on Computer Science and Application Engineering","acronym":"CSAE 2020","location":"Sanya China"},"container-title":["Proceedings of the 4th International Conference on Computer Science and Application Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3424978.3425032","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3424978.3425032","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:10Z","timestamp":1750197730000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3424978.3425032"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,20]]},"references-count":11,"alternative-id":["10.1145\/3424978.3425032","10.1145\/3424978"],"URL":"https:\/\/doi.org\/10.1145\/3424978.3425032","relation":{},"subject":[],"published":{"date-parts":[[2020,10,20]]},"assertion":[{"value":"2020-10-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}