{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:01:01Z","timestamp":1725559261757},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_1","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"1-7","source":"Crossref","is-referenced-by-count":3,"title":["A Formally Verified OS Kernel. Now What?"],"prefix":"10.1007","author":[{"given":"Gerwin","family":"Klein","sequence":"first","affiliation":[]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Boettcher, C., DeLong, R., Rushby, J., Sifre, W.: The MILS component integration approach to secure information sharing. In: 27th IEEE\/AIAA Digital Avionics Systems Conference (DASC), St. Paul MN (October 2008)","key":"1_CR1","DOI":"10.1109\/DASC.2008.4702758"},{"key":"1_CR2","series-title":"ENTCS","first-page":"25","volume-title":"4th WS Syst. Softw. Verification SSV\u201909","author":"A. Boyton","year":"2009","unstructured":"Boyton, A.: A verified shared capability model. In: Klein, G., Huuck, R., Schlich, B. (eds.) 4th WS Syst. Softw. Verification SSV\u201909, Aachen, Germany, October 2009. ENTCS, vol.\u00a0254, pp. 25\u201344. Elsevier, Amsterdam (2009)"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-540-87873-5_11","volume-title":"Verified Software: Theories, Tools, Experiments","author":"D. Elkaduwe","year":"2008","unstructured":"Elkaduwe, D., Klein, G., Elphinstone, K.: Verified protection model of the seL4 microkernel. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 99\u2013114. Springer, Heidelberg (2008)"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","first-page":"244","volume-title":"ITP\u201910","author":"A. Fox","year":"2010","unstructured":"Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the armv7 instruction set architecture. In: Kaufmann, M., Paulson, L. (eds.) ITP\u201910. LNCS, vol.\u00a06172, pp. 244\u2013259. Springer, Heidelberg (2010)"},{"key":"1_CR5","series-title":"October 2009","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/1629575.1629596","volume-title":"22nd SOSP","author":"G. Klein","year":"2009","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: 22nd SOSP, Big Sky, MT, USA. October 2009, pp. 207\u2013220. ACM, New York (2009)"},{"key":"1_CR6","first-page":"42","volume-title":"33rd POPL","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. In: Morrisett, J.G., Jones, S.L.P. (eds.) 33rd POPL, pp. 42\u201354. ACM, New York (2006)"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-00722-4_2","volume-title":"Compiler Construction","author":"M.O. Myreen","year":"2009","unstructured":"Myreen, M.O., Slind, K., Gordon, M.J.C.: Extensible proof-producing compilation. In: de Moor, O., Schwartzbach, M.I. (eds.) CC 2009. LNCS, vol.\u00a05501, pp. 2\u201316. Springer, Heidelberg (2009)"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"1_CR9","doi-asserted-by":"publisher","first-page":"1278","DOI":"10.1109\/PROC.1975.9939","volume":"63","author":"J.H. Saltzer","year":"1975","unstructured":"Saltzer, J.H., Schroeder, M.D.: The protection of information in computer systems. Proc. IEEE\u00a063, 1278\u20131308 (1975)","journal-title":"Proc. IEEE"},{"doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle\/HOL. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2006)","key":"1_CR10","DOI":"10.1007\/978-3-540-32275-7_26"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:46:59Z","timestamp":1606186019000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}