{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:02Z","timestamp":1761611222796},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540787990"},{"type":"electronic","value":"9783540788003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78800-3_9","type":"book-chapter","created":{"date-parts":[[2008,4,2]],"date-time":"2008-04-02T08:26:19Z","timestamp":1207124779000},"page":"109-123","source":"Crossref","is-referenced-by-count":19,"title":["Formal Pervasive Verification of a Paging Mechanism"],"prefix":"10.1007","author":[{"given":"Eyad","family":"Alkassar","sequence":"first","affiliation":[]},{"given":"Norbert","family":"Schirmer","sequence":"additional","affiliation":[]},{"given":"Artem","family":"Starostin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","unstructured":"Alkassar, E., Hillebrand, M., Knapp, S., Rusev, R., Tverdyshev, S.: Formal device and programming model for a serial interface. In: Proc. 4th International Verification Workshop (VERIFY). CEUR-WS Workshop Proc. (2007)"},{"issue":"4","key":"9_CR2","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/BF00243131","volume":"5","author":"W. Bevier","year":"1989","unstructured":"Bevier, W., Hunt Jr., W., Moore, J.S., Young, W.: An approach to systems verification. Journal of Automated Reasoning\u00a05(4), 411\u2013428 (1989)","journal-title":"Journal of Automated Reasoning"},{"issue":"4\u20135","key":"9_CR3","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/s10009-006-0204-6","volume":"8","author":"S. Beyer","year":"2006","unstructured":"Beyer, S., Jacobi, C., Kroening, D., Leinenbach, D., Paul, W.: Putting it all together: Formal verification of the VAMP. International Journal on Software Tools for Technology Transfer\u00a08(4\u20135), 411\u2013430 (2006)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"9_CR4","unstructured":"Condea, C.: Design and implementation of a page fault handler in C0. Master\u2019s thesis, Saarland University (July 2006)"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Gargano","year":"2005","unstructured":"Gargano, M., Hillebrand, M., Leinenbach, D., Paul, W.: 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":"9_CR6","doi-asserted-by":"crossref","unstructured":"Heiser, G., Elphinstone, K., Kuz, I., Klein, G., Petters, S.: Towards trustworthy computing systems: Taking microkernels to the next level. In: Operating Systems Review (July 2007)","DOI":"10.1145\/1278901.1278904"},{"key":"9_CR7","unstructured":"Hillebrand, M.: Address Spaces and Virtual Memory: Specification, Implementation, and Correctness. PhD thesis, Saarland University, Computer Science Department (June 2005)"},{"key":"9_CR8","first-page":"309","volume-title":"ICCD 2005","author":"M. Hillebrand","year":"2005","unstructured":"Hillebrand, M., In der Rieden, T., Paul, W.: Dealing with I\/O devices in the context of pervasive system verification. In: ICCD 2005, pp. 309\u2013316. IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"9_CR9","first-page":"165","volume-title":"Proc. 10th ACM SIGOPS","author":"M. Hohmuth","year":"2002","unstructured":"Hohmuth, M., Tews, H., Stephens, S.: Applying source-code verification to a microkernel: the vfiasco project. In: Proc. 10th ACM SIGOPS, pp. 165\u2013169. ACM Press, New York (2002)"},{"key":"9_CR10","unstructured":"Leinenbach, D., Petrova, E.: Pervasive compiler verification \u2013 from verified programs to verified systems. In: 3rd SSV 2008, Elsevier Science B. V (to appear, 2008)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Advances in Computer Systems Architecture","author":"P. Neumann","year":"2003","unstructured":"Neumann, P., Feiertag, R.: PSOS revisited. In: Omondi, A.R., Sedukhin, S. (eds.) ACSAC 2003. LNCS, vol.\u00a02823, Springer, Heidelberg (2003)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/978-3-540-76637-7","volume-title":"Theorem Proving in Higher Order Logics","author":"Z. Shao","year":"2007","unstructured":"Shao, Z., Yu, D., Ni, Z.: Using xcap to certify realistic systems code: Machine context management. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 189\u2013206. Springer, Heidelberg (2007)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle\/HOL. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (April 2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"9_CR14","unstructured":"Tuch, H., Klein, G.: Verifying the L4 virtual memory subsystem. In: Proc. NICTA Formal Methods Workshop on Operating Systems Verification, NICTA, pp. 73\u201397 (2004)"},{"key":"9_CR15","first-page":"97","volume-title":"Proc. 34th POPL","author":"H. Tuch","year":"2007","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Proc. 34th POPL, pp. 97\u2013108. ACM Press, New York (2007)"},{"issue":"2","key":"9_CR16","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1145\/358818.358825","volume":"23","author":"B. Walker","year":"1980","unstructured":"Walker, B., Kemmerer, R., Popek, G.: Specification and verification of the UCLA Unix security kernel. Commun. ACM\u00a023(2), 118\u2013131 (1980)","journal-title":"Commun. ACM"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78800-3_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:15:33Z","timestamp":1606184133000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78800-3_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540787990","9783540788003"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78800-3_9","relation":{},"subject":[]}}