{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T12:10:31Z","timestamp":1762863031103,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030255428"},{"type":"electronic","value":"9783030255435"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-25543-5_29","type":"book-chapter","created":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T12:03:09Z","timestamp":1562932989000},"page":"515-533","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Rely-Guarantee Reasoning About Concurrent Memory Management in Zephyr RTOS"],"prefix":"10.1007","author":[{"given":"Yongwang","family":"Zhao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"San\u00e1n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,7,12]]},"reference":[{"key":"29_CR1","unstructured":"The Zephyr Project. \n                      https:\/\/www.zephyrproject.org\/\n                      \n                    . Accessed Dec 2018"},{"key":"29_CR2","unstructured":"Common Criteria for Information Technology Security Evaluation (v3.1, Release 5). \n                      https:\/\/www.commoncriteriaportal.org\/\n                      \n                    . Accessed Apr 2017"},{"key":"29_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-540-78800-3_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Alkassar","year":"2008","unstructured":"Alkassar, E., Schirmer, N., Starostin, A.: Formal pervasive verification of a paging mechanism. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 109\u2013123. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-78800-3_9"},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-319-19458-5_2","volume-title":"Formal Methods for Industrial Critical Systems","author":"A Blanchard","year":"2015","unstructured":"Blanchard, A., Kosmatov, N., Lemerre, M., Loulergue, F.: A case study on formal verification of the anaxagoros hypervisor paging system with Frama-C. In: N\u00fa\u00f1ez, M., G\u00fcdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 15\u201330. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-19458-5_2"},{"key":"29_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-662-49665-7_13","volume-title":"Fundamental Approaches to Software Engineering","author":"P Bolignano","year":"2016","unstructured":"Bolignano, P., Jensen, T., Siles, V.: Modeling and abstraction of memory management in a hypervisor. In: Stevens, P., W\u0105sowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 214\u2013230. Springer, Heidelberg (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49665-7_13"},{"key":"29_CR6","doi-asserted-by":"crossref","unstructured":"Chen, H., Wu, X., Shao, Z., Lockerman, J., Gu, R.: Toward compositional verification of interruptible OS kernels and device drivers. In: Proceedings of 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 431\u2013447. ACM (2016)","DOI":"10.1145\/2980983.2908101"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-319-63139-4_9","volume-title":"Logic-Based Program Synthesis and Transformation","author":"B Fang","year":"2017","unstructured":"Fang, B., Sighireanu, M.: Hierarchical shape abstraction for analysis of free list memory allocators. In: Hermenegildo, M.V., Lopez-Garcia, P. (eds.) LOPSTR 2016. LNCS, vol. 10184, pp. 151\u2013167. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-63139-4_9"},{"key":"29_CR8","doi-asserted-by":"crossref","unstructured":"Fang, B., Sighireanu, M.: A refinement hierarchy for free list memory allocators. In: Proceedings of ACM SIGPLAN International Symposium on Memory Management, pp. 104\u2013114. ACM (2017)","DOI":"10.1145\/3156685.3092275"},{"issue":"12","key":"29_CR9","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/s11432-017-9280-9","volume":"61","author":"B Fang","year":"2018","unstructured":"Fang, B., et al.: Formal modelling of list based dynamic memory allocators. Sci. China Inf. Sci. 61(12), 103\u2013122 (2018)","journal-title":"Sci. China Inf. Sci."},{"issue":"2","key":"29_CR10","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10817-009-9124-y","volume":"42","author":"MDM Gallardo","year":"2009","unstructured":"Gallardo, M.D.M., Merino, P., San\u00e1n, D.: Model checking dynamic memory allocation in operating systems. J. Autom. Reasoning 42(2), 229\u2013264 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"29_CR11","unstructured":"Gu, R., et al.: CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: Proceedings of 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pp. 653\u2013669. USENIX Association, Savannah, GA (2016)"},{"key":"29_CR12","doi-asserted-by":"crossref","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: Proceedings of 22nd ACM SIGOPS Symposium on Operating Systems Principles (SOSP), pp. 207\u2013220. ACM Press (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"29_CR13","unstructured":"Klein, G., Tuch, H.: Towards verified virtual memory in L4. In: Proceedings of TPHOLs Emerging Trends, p. 16. Park City, Utah, USA, September 2004"},{"issue":"1","key":"29_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reasoning 41(1), 1\u201331 (2008)","journal-title":"J. Autom. Reasoning"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-319-21668-3_24","volume-title":"Computer Aided Verification","author":"W Mansky","year":"2015","unstructured":"Mansky, W., Garbuzov, D., Zdancewic, S.: An axiomatic specification for sequential memory models. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 413\u2013428. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-21668-3_24"},{"key":"29_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/11901433_22","volume-title":"Formal Methods and Software Engineering","author":"N Marti","year":"2006","unstructured":"Marti, N., Affeldt, R., Yonezawa, A.: Formal verification of the heap manager of an operating system using separation logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 400\u2013419. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11901433_22"},{"key":"29_CR17","doi-asserted-by":"crossref","unstructured":"Saraswat, V.A., Jagadeesan, R., Michael, M., von Praun, C.: A theory of memory models. In: Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), pp. 161\u2013172. ACM (2007)","DOI":"10.1145\/1229428.1229469"},{"key":"29_CR18","doi-asserted-by":"crossref","unstructured":"Su, W., Abrial, J.R., Pu, G., Fang, B.: Formal development of a real-time operating system memory manager. In: Proceedings of International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 130\u2013139 (2016)","DOI":"10.1109\/ICECCS.2015.24"},{"issue":"2","key":"29_CR19","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s10817-009-9122-0","volume":"42","author":"H Tews","year":"2009","unstructured":"Tews, H., V\u00f6lp, M., Weber, T.: Formal memory models for the verification of low-level operating-system code. J. Autom. Reasoning 42(2), 189\u2013227 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"29_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-642-35308-6_13","volume-title":"Certified Programs and Proofs","author":"A Vaynberg","year":"2012","unstructured":"Vaynberg, A., Shao, Z.: Compositional verification of a baby virtual memory manager. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 143\u2013159. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-35308-6_13"},{"issue":"3","key":"29_CR21","doi-asserted-by":"publisher","first-page":"22:1","DOI":"10.1145\/2487241.2487248","volume":"60","author":"J \u0160ev\u010d\u00edk","year":"2013","unstructured":"\u0160ev\u010d\u00edk, J., Vafeiadis, V., Nardelli, F.Z., Jagannathan, S., Sewell, P.: CompCertTSO: a verified compiler for relaxed-memory concurrency. J. ACM 60(3), 22:1\u201322:50 (2013)","journal-title":"J. ACM"},{"key":"29_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-319-41540-6_4","volume-title":"Computer Aided Verification","author":"F Xu","year":"2016","unstructured":"Xu, F., Fu, M., Feng, X., Zhang, X., Zhang, H., Li, Z.: A practical verification framework for preemptive OS kernels. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 59\u201379. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-41540-6_4"},{"key":"29_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-36575-3_25","volume-title":"Programming Languages and Systems","author":"D Yu","year":"2003","unstructured":"Yu, D., Hamid, N.A., Shao, Z.: Building certified libraries for PCC: dynamic storage allocation. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 363\u2013379. Springer, Heidelberg (2003). \n                      https:\/\/doi.org\/10.1007\/3-540-36575-3_25"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-25543-5_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,12]],"date-time":"2019-07-12T12:10:54Z","timestamp":1562933454000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-25543-5_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030255428","9783030255435"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-25543-5_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"12 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New York City, NY","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav0","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2019\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"258","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}