{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:13:19Z","timestamp":1774987999061,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642353079","type":"print"},{"value":"9783642353086","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35308-6_13","type":"book-chapter","created":{"date-parts":[[2012,11,8]],"date-time":"2012-11-08T03:20:18Z","timestamp":1352344818000},"page":"143-159","source":"Crossref","is-referenced-by-count":12,"title":["Compositional Verification of a Baby Virtual Memory Manager"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Vaynberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s10817-009-9123-z","volume":"42","author":"E. Alkassar","year":"2009","unstructured":"Alkassar, E., Hillebrand, M.A., Leinenbach, D.C., Schirmer, N.W., Starostin, A., Tsyban, A.: Balancing the load: Leveraging a semantics stack for systems verification. Journal of Automated Reasoning: OS Verification\u00a042, 389\u2013454 (2009)","journal-title":"Journal of Automated Reasoning: OS Verification"},{"key":"13_CR2","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.W., Starostin, A.: Formal Pervasive Verification of a Paging Mechanism. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 109\u2013123. Springer, Heidelberg (2008)"},{"key":"13_CR3","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/1250734.1250743","volume-title":"Proc. PLDI 2007","author":"H. Cai","year":"2007","unstructured":"Cai, H., Shao, Z., Vaynberg, A.: Certified self-modifying code. In: Proc. PLDI 2007, pp. 66\u201377. ACM, New York (2007)"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P., Yang, H.: Local action and abstract separation logic. In: Proc. LICS 2007, pp. 366\u2013378 (July 2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"13_CR5","unstructured":"Coq Development Team. The Coq proof assistant reference manual. The Coq release v8.0 (October 2005)"},{"key":"13_CR6","unstructured":"Elphinstone, K., Klein, G., Derrin, P., Roscoe, T., Heiser, G.: Towards a practical, verified kernel. In: Proc. HoTOS 2007, San Diego, CA, USA (May 2007)"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z., Dong, Y., Guo, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. In: Proc. PLDI 2008, pp. 170\u2013182. ACM (2008)","DOI":"10.1145\/1375581.1375603"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z., Vaynberg, A., Xiang, S., Ni, Z.: Modular verification of assembly code with stack-based control abstractions. In: PLDI 2006, pp. 401\u2013414 (June 2006)","DOI":"10.1145\/1133981.1134028"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11541868_1","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Gargano","year":"2005","unstructured":"Gargano, M., Hillebrand, M.A., Leinenbach, D., Paul, W.J.: On the Correctness of Operating System Kernels. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 1\u201316. Springer, Heidelberg (2005)"},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Gu, L., Vaynberg, A., Ford, B., Shao, Z., Costanzo, D.: Certikos: A certified kernel for secure cloud computing. In: Proc. APSys 2011. ACM (2011)","DOI":"10.1145\/2103799.2103803"},{"key":"13_CR11","unstructured":"In der Rieden, T.: Verified Linking for Modular Kernel Verification. PhD thesis, Saarland University, Computer Science Department (November 2009)"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: formal verification of an OS kernel. In: Proc. SOSP 2009, pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"13_CR13","unstructured":"Klein, G., Tuch, H.: Towards verified virtual memory in l4. In: TPHOLs Emerging Trends 2004, Park City, Utah, USA (September 2004)"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-87873-5_6","volume-title":"Verified Software: Theories, Tools, Experiments","author":"R. Kolanski","year":"2008","unstructured":"Kolanski, R., Klein, G.: Mapped Separation Logic. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 15\u201329. Springer, Heidelberg (2008)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"McCreight, A., Shao, Z., Lin, C., Li, L.: A general framework for certifying garbage collectors and their mutators. In: Proc. PLDI 2007, pp. 468\u2013479 (2007)","DOI":"10.1145\/1250734.1250788"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL 2004, pp. 268\u2013280 (January 2004)","DOI":"10.1145\/982962.964024"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. LICS 2002, pp. 55\u201374 (July 2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"13_CR18","unstructured":"Starostin, A.: Formal Verification of Demand Paging. PhD thesis, Saarland University, Computer Science Department (March 2010)"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Vaynberg, A., Shao, Z.: Compositional verification of BabyVMM (extended version and Coq proof). Technical Report YALEU\/DCS\/TR-1463, Yale University (October 2012), http:\/\/flint.cs.yale.edu\/publications\/babyvmm.html","DOI":"10.1007\/978-3-642-35308-6_13"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35308-6_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,20]],"date-time":"2025-04-20T12:19:38Z","timestamp":1745151578000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35308-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642353079","9783642353086"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35308-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}