{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:01:22Z","timestamp":1750309282912,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":17,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,9,22]],"date-time":"2023-09-22T00:00:00Z","timestamp":1695340800000},"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":[[2023,9,22]]},"DOI":"10.1145\/3641584.3641769","type":"proceedings-article","created":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T22:44:43Z","timestamp":1718405083000},"page":"1231-1236","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Verifying Kernel Abstract Layer of HarmonyOS with Projection Temporal Logic"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-4753-3908","authenticated-orcid":false,"given":"Ye","family":"Tian","sequence":"first","affiliation":[{"name":"Xi'an University of Posts and Telecommunications, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7293-4510","authenticated-orcid":false,"given":"Xinfeng","family":"Shu","sequence":"additional","affiliation":[{"name":"Trusted Software Experimental Team, Xi'an University of Posts and Telecommunications, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,14]]},"reference":[{"volume-title":"seL4: Formal verification of an OS kernel[C]\/\/Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. 2009: 207-220","author":"Klein G","key":"e_1_3_2_1_1_1","unstructured":"Klein G, Elphinstone K, Heiser G, seL4: Formal verification of an OS kernel[C]\/\/Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. 2009: 207-220."},{"volume-title":"Experiments: Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings 2. Springer Berlin Heidelberg","author":"Alkassar E","key":"e_1_3_2_1_2_1","unstructured":"Alkassar E, Hillebrand M A, Leinenbach D, The Verisoft approach to systems verification[C]\/\/Verified Software: Theories, Tools, Experiments: Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings 2. Springer Berlin Heidelberg, 2008: 209-224."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103621.2103690"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Elphinstone K Heiser G. From L3 to seL4 what have we learnt in 20 years of L4 microkernels?[C]\/\/Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles. 2013: 133-150.","DOI":"10.1145\/2517349.2522720"},{"key":"e_1_3_2_1_5_1","volume-title":"Real world haskell: Code you can believe in[M]. \" O'Reilly Media","author":"O'Sullivan B","year":"2008","unstructured":"O'Sullivan B, Goerzen J, Stewart D B. Real world haskell: Code you can believe in[M]. \" O'Reilly Media, Inc.\", 2008."},{"key":"e_1_3_2_1_6_1","volume-title":"a proof assistant for higher-order logic[M]","author":"Isabelle HOL","year":"2002","unstructured":"Isabelle\/HOL: a proof assistant for higher-order logic[M]. Berlin, Heidelberg: Springer Berlin Heidelberg, 2002."},{"volume-title":"Theorem Proving: Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings 2. Springer Berlin Heidelberg","author":"Sewell T","key":"e_1_3_2_1_7_1","unstructured":"Sewell T, Winwood S, Gammie P, seL4 enforces integrity[C]\/\/Interactive Theorem Proving: Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings 2. Springer Berlin Heidelberg, 2011: 325-340."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2012.41"},{"key":"e_1_3_2_1_9_1","volume-title":"Verifying shadow page table algorithms[C]\/\/Formal Methods in Computer Aided Design","author":"Alkassar E","year":"2010","unstructured":"Alkassar E, Cohen E, Hillebrand M, Verifying shadow page table algorithms[C]\/\/Formal Methods in Computer Aided Design. IEEE, 2010: 267-270."},{"key":"e_1_3_2_1_10_1","volume-title":"Proving memory separation in a microkernel by code level verification[C]\/\/2011 14th IEEE International Symposium on Object\/Component\/Service-Oriented Real-Time Distributed Computing Workshops","author":"Baumann C","year":"2011","unstructured":"Baumann C, Bormer T, Blasum H, Proving memory separation in a microkernel by code level verification[C]\/\/2011 14th IEEE International Symposium on Object\/Component\/Service-Oriented Real-Time Distributed Computing Workshops. IEEE, 2011: 25-32."},{"volume-title":"CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings 2. Springer Berlin Heidelberg","author":"Vaynberg A","key":"e_1_3_2_1_11_1","unstructured":"Vaynberg A, Shao Z. Compositional verification of a baby virtual memory manager[C]\/\/Certified Programs and Proofs: Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012. Proceedings 2. Springer Berlin Heidelberg, 2012: 143-159."},{"volume-title":"A rely-guarantee-based simulation for verifying concurrent program transformations[C]\/\/Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 2012: 455-468","author":"Liang H","key":"e_1_3_2_1_12_1","unstructured":"Liang H, Feng X, Fu M. A rely-guarantee-based simulation for verifying concurrent program transformations[C]\/\/Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 2012: 455-468."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-007-0062-z"},{"issue":"03","key":"e_1_3_2_1_14_1","doi-asserted-by":"crossref","first-page":"366","DOI":"10.3724\/SP.J.1001.2011.03918","article-title":"Complete Axiomatic Systems for Finite-Time Projection Temporal Logic","volume":"22","author":"Shu","year":"2011","unstructured":"Shu, Xinfeng, and Duan, Zhenhua. \"Complete Axiomatic Systems for Finite-Time Projection Temporal Logic.\" Journal of Software, 2011, 22(03): 366-380.","journal-title":"Journal of Software"},{"issue":"04","key":"e_1_3_2_1_15_1","first-page":"680","article-title":"Axiomatic System and Formal Verification of Projection Temporal Logic","volume":"36","author":"Shu","year":"2009","unstructured":"Shu, Xinfeng, and Duan, Zhenhua. \"Axiomatic System and Formal Verification of Projection Temporal Logic.\" Journal of Xidian University, 2009, 36(04): 680-685+729.","journal-title":"Journal of Xidian University"},{"key":"e_1_3_2_1_16_1","volume-title":"Formal verification of a small real-time operating system[J]","author":"Schmidt M D","year":"2011","unstructured":"Schmidt M D. Formal verification of a small real-time operating system[J]. 2011."},{"key":"e_1_3_2_1_17_1","first-page":"65","article-title":"Assigning meanings to programs[J]","volume":"1993","author":"Floyd R W","unstructured":"[1] Floyd R W. Assigning meanings to programs[J]. Program Verification: Fundamental Issues in Computer Science, 1993: 65-81.","journal-title":"Program Verification: Fundamental Issues in Computer Science"}],"event":{"name":"AIPR 2023: 2023 6th International Conference on Artificial Intelligence and Pattern Recognition","acronym":"AIPR 2023","location":"Xiamen China"},"container-title":["2023 6th International Conference on Artificial Intelligence and Pattern Recognition (AIPR)"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3641584.3641769","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3641584.3641769","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:03:12Z","timestamp":1750291392000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3641584.3641769"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,22]]},"references-count":17,"alternative-id":["10.1145\/3641584.3641769","10.1145\/3641584"],"URL":"https:\/\/doi.org\/10.1145\/3641584.3641769","relation":{},"subject":[],"published":{"date-parts":[[2023,9,22]]},"assertion":[{"value":"2024-06-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}