{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:09:53Z","timestamp":1750219793087,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,7,28]],"date-time":"2023-07-28T00:00:00Z","timestamp":1690502400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"State Grid Corporation of China Headquarters Management Technology Project","award":["5108-202118056A-0-0-00"],"award-info":[{"award-number":["5108-202118056A-0-0-00"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,7,28]]},"DOI":"10.1145\/3609703.3609714","type":"proceedings-article","created":{"date-parts":[[2023,8,16]],"date-time":"2023-08-16T16:24:31Z","timestamp":1692203071000},"page":"65-70","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Survey of the Formal Verification of Operating Systems in Power Monitoring System"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-4465-6818","authenticated-orcid":false,"given":"Kangle","family":"Yang","sequence":"first","affiliation":[{"name":"Nanjing NARI Information and Communication Technology Co., Ltd., China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3365-5655","authenticated-orcid":false,"given":"Jianye","family":"Yu","sequence":"additional","affiliation":[{"name":"Nanjing NARI Information and Communication Technology Co., Ltd., China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3024-7798","authenticated-orcid":false,"given":"Xinshen","family":"Wei","sequence":"additional","affiliation":[{"name":"Nanjing NARI Information and Communication Technology Co., Ltd., China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7959-4910","authenticated-orcid":false,"given":"Feng","family":"You","sequence":"additional","affiliation":[{"name":"Nanjing NARI Information and Communication Technology Co., Ltd., China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7714-3809","authenticated-orcid":false,"given":"Haidong","family":"Huang","sequence":"additional","affiliation":[{"name":"State Grid Jiangsu Electric Power Co., Ltd., China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6185-5115","authenticated-orcid":false,"given":"Xuesong","family":"Huo","sequence":"additional","affiliation":[{"name":"State Grid Jiangsu Electric Power Co., Ltd., China"}]}],"member":"320","published-online":{"date-parts":[[2023,8,16]]},"reference":[{"volume-title":"COMMUNICATIONS OF THE ACM","author":"Hoare C.","key":"e_1_3_2_1_1_1","unstructured":"C. Hoare , \u201c AN AXIOMATIC BASIS FOR COMPUTER PROGRAMMING ,\u201d COMMUNICATIONS OF THE ACM , vol. 12 , no. 10, pp. 576\u2013&, 1969. C. Hoare, \u201cAN AXIOMATIC BASIS FOR COMPUTER PROGRAMMING,\u201d COMMUNICATIONS OF THE ACM, vol. 12, no. 10, pp. 576\u2013&, 1969."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45465-9_51"},{"volume-title":"Resources, concurrency, and local reasoning","author":"O'Hearn P. W.","key":"e_1_3_2_1_4_1","unstructured":"P. W. O'Hearn , \u201c Resources, concurrency, and local reasoning ,\u201d theoretical computer science, vol. 375 , no. 1-3, pp. 271\u2013307, 2004. P. W. O'Hearn, \u201cResources, concurrency, and local reasoning,\u201d theoretical computer science, vol. 375, no. 1-3, pp. 271\u2013307, 2004."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_1_8_1","volume-title":"Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods","author":"Yuan Y.","year":"1999","unstructured":"Y. Yuan , P. Manolios , and L. Lamport , \u201c Model checking tla+ specifications ,\u201d in Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods , 1999 . Y. Yuan, P. Manolios, and L. Lamport, \u201cModel checking tla+ specifications,\u201d in Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, 1999."},{"issue":"1","key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","first-page":"595","DOI":"10.1145\/2775051.2676975","article-title":"Deep specifications and certified abstraction layers","volume":"50","author":"Chun Shu","year":"2015","unstructured":"Xiongnan, Newman, Ronghui, Ramananandro, Tahina, Weng, Shu Chun , Shao, Zhong, and K. and , \u201c Deep specifications and certified abstraction layers ,\u201d ACM SIGPLAN Notices: A Monthly Publication of the Special Interest Group on Programming Languages , vol. 50 , no. 1 , pp. 595 \u2013 608 , 2015 . Xiongnan, Newman, Ronghui, Ramananandro, Tahina, Weng, Shu Chun, Shao, Zhong, and K. and, \u201cDeep specifications and certified abstraction layers,\u201d ACM SIGPLAN Notices: A Monthly Publication of the Special Interest Group on Programming Languages, vol. 50, no. 1, pp. 595\u2013608, 2015.","journal-title":"ACM SIGPLAN Notices: A Monthly Publication of the Special Interest Group on Programming Languages"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/291251.289440"},{"volume-title":"ACM SIGPLAN Notices: A Monthly Publication of the Special Interest Group on Programming Languages","year":"2016","key":"e_1_3_2_1_11_1","unstructured":"\u201c Cogent: Verifying high-assurance file system implementations ,\u201d ACM SIGPLAN Notices: A Monthly Publication of the Special Interest Group on Programming Languages , 2016 . \u201cCogent: Verifying high-assurance file system implementations,\u201d ACM SIGPLAN Notices: A Monthly Publication of the Special Interest Group on Programming Languages, 2016."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360562"},{"key":"e_1_3_2_1_13_1","volume-title":"\u201cCertikos: an extensible architecture for building certified concurrent os kernels","author":"Gu R.","year":"2016","unstructured":"R. Gu , Z. Shao , H. Chen , X. Wu , J. Kim , berg, and D. Costanzo , \u201cCertikos: an extensible architecture for building certified concurrent os kernels ,\u201d 2016 . R. Gu, Z. Shao, H. Chen, X. Wu, J. Kim, berg, and D. Costanzo, \u201cCertikos: an extensible architecture for building certified concurrent os kernels,\u201d 2016."},{"key":"e_1_3_2_1_14_1","volume-title":"Building a file system with fscq infrastructure","author":"Chen H.","year":"2015","unstructured":"H. Chen , \u201c Building a file system with fscq infrastructure ,\u201d 2015 . H. Chen, \u201cBuilding a file system with fscq infrastructure,\u201d 2015."},{"key":"e_1_3_2_1_15_1","volume-title":"Stephanie, \u201cCertifying checksum-based logging in the rapidfscq crash-safe filesystem","author":"M. E. M.","year":"2016","unstructured":"M. E. M. I. o. T. Wang , Stephanie, \u201cCertifying checksum-based logging in the rapidfscq crash-safe filesystem ,\u201d 2016 . M. E. M. I. o. T. Wang, Stephanie, \u201cCertifying checksum-based logging in the rapidfscq crash-safe filesystem,\u201d 2016."},{"key":"e_1_3_2_1_16_1","volume-title":"Special A Specification And Assertion Language","author":"Robinson L.","year":"1976","unstructured":"L. Robinson and O. Roubine , \u201c Special - a specification and assertion language ,\u201d Special A Specification And Assertion Language , 1976 . L. Robinson and O. Roubine, \u201cSpecial - a specification and assertion language,\u201d Special A Specification And Assertion Language, 1976."},{"key":"e_1_3_2_1_17_1","volume-title":"An overview of the scala programming language","author":"Odersky M.","year":"2008","unstructured":"M. Odersky , P. Altherr , V. Cremet , B. Emir , and M. Zenger , \u201c An overview of the scala programming language ,\u201d epfl, 2008 . M. Odersky, P. Altherr, V. Cremet, B. Emir, and M. Zenger, \u201cAn overview of the scala programming language,\u201d epfl, 2008."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_3_2_1_19_1","volume-title":"Z3: an efficient smt solver","author":"Moura L. D.","year":"2008","unstructured":"L. D. Moura and N. Bjrner , \u201c Z3: an efficient smt solver ,\u201d Springer , 2008 . L. D. Moura and N. Bjrner, \u201cZ3: an efficient smt solver,\u201d Springer, 2008."},{"issue":"07","key":"e_1_3_2_1_20_1","first-page":"769","article-title":"Smt brief description of solution technology","author":"Jing J.","year":"2015","unstructured":"J. Jing , F. Ma , and J. Zhang , \u201c Smt brief description of solution technology ,\u201d Journal of Frontiers of Computer Science and Technology , no. 07 , pp. 769 \u2013 780 , 2015 . J. Jing, F. Ma, and J. Zhang, \u201cSmt brief description of solution technology,\u201d Journal of Frontiers of Computer Science and Technology, no. 07, pp. 769\u2013780, 2015.","journal-title":"Journal of Frontiers of Computer Science and Technology"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"key":"e_1_3_2_1_22_1","volume-title":"Sensitive","author":"Baumann C.","year":"2009","unstructured":"C. Baumann and T. Bormer , \u201c Verifying the pikeos microkernel: First results in the verisoftxt avionics project ,\u201d Sensitive , 2009 . C. Baumann and T. Bormer, \u201cVerifying the pikeos microkernel: First results in the verisoftxt avionics project,\u201d Sensitive, 2009."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"issue":"5","key":"e_1_3_2_1_24_1","first-page":"563576","article-title":"The compcert c verified compiler: Documentation and user's manual","volume":"16","author":"Leroy X.","year":"2015","unstructured":"X. Leroy , \u201c The compcert c verified compiler: Documentation and user's manual ,\u201d Inria , vol. 16 , no. 5 , p. 563576 , 2015 . X. Leroy, \u201cThe compcert c verified compiler: Documentation and user's manual,\u201d Inria, vol. 16, no. 5, p. 563576, 2015.","journal-title":"Inria"},{"key":"e_1_3_2_1_25_1","first-page":"30","article-title":"An abstract stack based approach to verified compositional compilation to machine code","volume":"3","author":"Wang Y.","year":"2019","unstructured":"Y. Wang ., P. Wilke ., and Z. Shao ., \u201c An abstract stack based approach to verified compositional compilation to machine code ,\u201d ACM on Programming Languages , vol. 3 , p. 30 , 2019 . Y. Wang., P. Wilke., and Z. Shao., \u201cAn abstract stack based approach to verified compositional compilation to machine code,\u201d ACM on Programming Languages, vol. 3, p. 30, 2019.","journal-title":"ACM on Programming Languages"},{"key":"e_1_3_2_1_26_1","volume-title":"Compcertelf: Verifjed separate compilation of c programs into elf object files","author":"Wang Y.","year":"2020","unstructured":"Y. Wang , X. Xu , P. Wilke , and Z. Shao , \u201c Compcertelf: Verifjed separate compilation of c programs into elf object files ,\u201d p. 28, November 2020 . Y. Wang, X. Xu, P. Wilke, and Z. Shao, \u201cCompcertelf: Verifjed separate compilation of c programs into elf object files,\u201d p. 28, November 2020."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314595"},{"key":"e_1_3_2_1_28_1","first-page":"461","volume-title":"A verified generational garbage collector for cakeml","author":"Ericsson A.","year":"2017","unstructured":"A. Ericsson , M. Myreen , and J. Pohjola , \u201c A verified generational garbage collector for cakeml ,\u201d 08 2017 , pp. 444\u2013 461 . A. Ericsson, M. Myreen, and J. Pohjola, \u201cA verified generational garbage collector for cakeml,\u201d 08 2017, pp. 444\u2013461."},{"key":"e_1_3_2_1_29_1","volume-title":"Verification of the ucla security kernel: abstract model, mapping, theorem generation and proof","author":"Kemmerer R.","year":"2021","unstructured":"R. Kemmerer , \u201c Verification of the ucla security kernel: abstract model, mapping, theorem generation and proof ,\u201d 2021 . R. Kemmerer, \u201cVerification of the ucla security kernel: abstract model, mapping, theorem generation and proof,\u201d 2021."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676975"},{"key":"e_1_3_2_1_31_1","first-page":"514","volume-title":"Cham","author":"Guo X.","year":"2019","unstructured":"X. Guo , M. Lesourd , M. Liu , L. Rieg , and Z. Shao , \u201c Integrating formal schedulability analysis into a verified os kernel ,\u201d in Computer Aided Verification, I. Dillig and S. Tasiran, Eds. Cham : Springer International Publishing , 2019 , pp. 496\u2013 514 . X. Guo, M. Lesourd, M. Liu, L. Rieg, and Z. Shao, \u201cIntegrating formal schedulability analysis into a verified os kernel,\u201d in Computer Aided Verification, I. Dillig and S. Tasiran, Eds. Cham: Springer International Publishing, 2019, pp. 496\u2013514."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371088"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2797022.2797042"},{"key":"e_1_3_2_1_35_1","volume-title":"The clustered multikernel: An approach to formal verification of multiprocessor os kernels","author":"Tessin M. V.","year":"2012","unstructured":"M. V. Tessin , \u201c The clustered multikernel: An approach to formal verification of multiprocessor os kernels ,\u201d ws on systems for future multi, 2012 . M. V. Tessin, \u201cThe clustered multikernel: An approach to formal verification of multiprocessor os kernels,\u201d ws on systems for future multi, 2012."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3378426"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3421473.3421475"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"e_1_3_2_1_40_1","first-page":"42","volume-title":"22nd International Conference, TPHOLs 2009","volume":"5674","author":"Moskal M.","year":"2009","unstructured":"M. Moskal , T. Santen , and W. Schulte , \u201c Vcc: A practical system for verifying concurrent c,\u201d in Theorem Proving in Higher Order Logics , 22nd International Conference, TPHOLs 2009 , ser. Lecture Notes in Computer Science , vol. 5674 . Springer, January 2009 , pp. 23\u2013 42 . M. Moskal, T. Santen, and W. Schulte, \u201cVcc: A practical system for verifying concurrent c,\u201d in Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, ser. Lecture Notes in Computer Science, vol. 5674. Springer, January 2009, pp. 23\u201342."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2576235"},{"key":"e_1_3_2_1_42_1","first-page":"79","volume-title":"Cham","author":"Xu F.","year":"2016","unstructured":"F. Xu , M. Fu , X. Feng , X. Zhang , H. Zhang , and Z. Li , \u201c A practical verification framework for preemptive os kernels ,\u201d in Computer Aided Verification, S. Chaudhuri and A. Farzan, Eds. Cham : Springer International Publishing , 2016 , pp. 59\u2013 79 . F. Xu, M. Fu, X. Feng, X. Zhang, H. Zhang, and Z. Li, \u201cA practical verification framework for preemptive os kernels,\u201d in Computer Aided Verification, S. Chaudhuri and A. Farzan, Eds. Cham: Springer International Publishing, 2016, pp. 59\u201379."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3357223.3362739"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485474"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394799"},{"key":"e_1_3_2_1_46_1","first-page":"411","article-title":"A hybrid formal verification system in coq for ensuring the reliability and security of ethereum-based service smart contracts","volume":"8","author":"Yang Z.","year":"2020","unstructured":"Z. Yang , H. Lei , and W. Qian , \u201c A hybrid formal verification system in coq for ensuring the reliability and security of ethereum-based service smart contracts ,\u201d IEEE Access , vol. 8 , pp. 21 411 \u2013 421 436, 2020 . Z. Yang, H. Lei, and W. Qian, \u201cA hybrid formal verification system in coq for ensuring the reliability and security of ethereum-based service smart contracts,\u201d IEEE Access, vol. 8, pp. 21 411\u201321 436, 2020.","journal-title":"IEEE Access"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2018.2880692"},{"volume-title":"Communications of the Acm","author":"Philip Wadler","key":"e_1_3_2_1_48_1","unstructured":"Wadler and Philip , \u201c Propositions as types ,\u201d Communications of the Acm , vol. 58 , no. 12, 2015. Wadler and Philip, \u201cPropositions as types,\u201d Communications of the Acm, vol. 58, no. 12, 2015."},{"key":"e_1_3_2_1_49_1","volume-title":"Scilla: a Smart Contract Intermediate-Level LAnguage","author":"Sergey I.","year":"1801","unstructured":"I. Sergey , A. Kumar , and A. Hobor , \u201c Scilla: a Smart Contract Intermediate-Level LAnguage ,\u201d arXiv e-prints, p. arXiv: 1801 .00687, Jan. 2018. I. Sergey, A. Kumar, and A. Hobor, \u201cScilla: a Smart Contract Intermediate-Level LAnguage,\u201d arXiv e-prints, p. arXiv:1801.00687, Jan. 2018."},{"key":"e_1_3_2_1_50_1","volume-title":"Simplicity: A New Language for Blockchains","author":"O'Connor R.","year":"2017","unstructured":"R. O'Connor , \u201c Simplicity: A New Language for Blockchains ,\u201d arXiv e-prints, p. arXiv: 1711.03028, Nov. 2017 . R. O'Connor, \u201cSimplicity: A New Language for Blockchains,\u201d arXiv e-prints, p. arXiv:1711.03028, Nov. 2017."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993611"}],"event":{"name":"PRIS 2023: 2023 5th International Conference on Pattern Recognition and Intelligent Systems","acronym":"PRIS 2023","location":"Shenyang China"},"container-title":["Proceedings of the 2023 5th International Conference on Pattern Recognition and Intelligent Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3609703.3609714","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3609703.3609714","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:01Z","timestamp":1750178281000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3609703.3609714"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,28]]},"references-count":51,"alternative-id":["10.1145\/3609703.3609714","10.1145\/3609703"],"URL":"https:\/\/doi.org\/10.1145\/3609703.3609714","relation":{},"subject":[],"published":{"date-parts":[[2023,7,28]]},"assertion":[{"value":"2023-08-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}