{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T21:05:06Z","timestamp":1780607106589,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":9,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,10,22]],"date-time":"2018-10-22T00:00:00Z","timestamp":1540166400000},"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":[[2018,10,22]]},"DOI":"10.1145\/3207677.3277971","type":"proceedings-article","created":{"date-parts":[[2018,10,18]],"date-time":"2018-10-18T10:19:29Z","timestamp":1539857969000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Verification of GP Specification based Embedded Operating System"],"prefix":"10.1145","author":[{"given":"Haiyong","family":"Sun","sequence":"first","affiliation":[{"name":"School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lei","family":"Qiao","sequence":"additional","affiliation":[{"name":"Beijing Institute of Control Engineering, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zheng","family":"Yang","sequence":"additional","affiliation":[{"name":"School of Information and Software Engineering, University of Electronic Science and Technology of China, Chengdu, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,10,22]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"GlobalPlatform. 2017. TEESystem Architecture Version 1.1 https:\/\/globalplatform.org\/specs-library\/?filter-committee=tee."},{"key":"e_1_3_2_1_2_1","unstructured":"GlobalPlatform.2016. TEE Internal Core API Specification Version 1.1.2 https:\/\/globalplatform.org\/specs-library\/?filter-committee=tee."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","unstructured":"R. Gu J. Koenig T. Ram and Z. Shao. 2015. Deep specifications and certified abstraction layers. ACM SIGPLAN Notices 50(1). ACM. 10.1145\/2775051.2676975","DOI":"10.1145\/2775051.2676975"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87873-5_18"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11741060_9"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/2021296.2021322"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","unstructured":"X. Yang. 2014. Trust-E: A Trusted Embedded Operating System Based on the ARM Trustzone. Ubiquitous Intelligence and Computing. 10.1109\/UIC-ATC-ScalCom.2014.15","DOI":"10.1109\/UIC-ATC-ScalCom.2014.15"},{"key":"e_1_3_2_1_9_1","unstructured":"X. Leroy. 2005-2016. The CompCert verified compiler. http:\/\/compcert. inria.fr."}],"event":{"name":"CSAE '18: The 2nd International Conference on Computer Science and Application Engineering","location":"Hohhot China","acronym":"CSAE '18"},"container-title":["Proceedings of the 2nd International Conference on Computer Science and Application Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3207677.3277971","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3207677.3277971","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T20:41:09Z","timestamp":1780605669000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3207677.3277971"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,22]]},"references-count":9,"alternative-id":["10.1145\/3207677.3277971","10.1145\/3207677"],"URL":"https:\/\/doi.org\/10.1145\/3207677.3277971","relation":{},"subject":[],"published":{"date-parts":[[2018,10,22]]},"assertion":[{"value":"2018-10-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}