{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,13]],"date-time":"2026-04-13T11:07:24Z","timestamp":1776078444037,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642180699","type":"print"},{"value":"9783642180705","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-18070-5_1","type":"book-chapter","created":{"date-parts":[[2011,1,15]],"date-time":"2011-01-15T09:18:02Z","timestamp":1295083082000},"page":"1-9","source":"Crossref","is-referenced-by-count":2,"title":["From a Proven Correct Microkernel to Trustworthy Large Systems"],"prefix":"10.1007","author":[{"given":"June","family":"Andronick","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1504\/IJES.2006.014859","volume":"2","author":"J. Alves-Foss","year":"2006","unstructured":"Alves-Foss, J., Oman, P.W., Taylor, C., Harrison, S.: The MILS architecture for high-assurance embedded systems. Int. J. Emb. Syst.\u00a02, 239\u2013247 (2006)","journal-title":"Int. J. Emb. Syst."},{"key":"1_CR2","unstructured":"Andronick, J., Greenaway, D., Elphinstone, K.: Towards proving security in the presence of large untrusted components. In: Klein, G., Huuck, R., Schlich, B. (eds.) 5th SSV, Vancouver, Canada, USENIX (October 2010)"},{"key":"1_CR3","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/365230.365252","volume":"9","author":"J.B. Dennis","year":"1966","unstructured":"Dennis, J.B., Van Horn, E.C.: Programming semantics for multiprogrammed computations. CACM\u00a09, 143\u2013155 (1966)","journal-title":"CACM"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Heiser, G., Andronick, J., Elphinstone, K., Klein, G., Kuz, I., Ryzhyk, L.: The road to trustworthy systems. In: 5th WS Scalable Trusted Comput., Chicago, IL, USA (October 2010)","DOI":"10.1145\/1867635.1867638"},{"issue":"6","key":"1_CR5","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G. Klein","year":"2010","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Heiser, G., 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. CACM\u00a053(6), 107\u2013115 (2010)","journal-title":"CACM"},{"key":"1_CR6","first-page":"207","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, pp. 207\u2013220. ACM, New York (October 2009)"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Kuz, I., Klein, G., Lewis, C., Walker, A.: capDL: A language for describing capability-based systems. In: 1st APSys, New Delhi, India (to appear, August 2010)","DOI":"10.1145\/1851276.1851284"},{"issue":"9","key":"1_CR8","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/234215.234473","volume":"39","author":"J. Liedtke","year":"1996","unstructured":"Liedtke, J.: Towards real microkernels. CACM\u00a039(9), 70\u201377 (1996)","journal-title":"CACM"},{"key":"1_CR9","series-title":"LNCS","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"1_CR10","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"},{"key":"1_CR11","unstructured":"Tuch, H.: Formal Memory Models for Verifying C Systems Code. PhD thesis, School Comp. Sci. & Engin., University NSW, Sydney 2052, Australia (August 2008)"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) 34th POPL, Nice, France, pp. 97\u2013108 (January 2007)","DOI":"10.1145\/1190216.1190234"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/978-3-642-03359-9_34","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Winwood","year":"2009","unstructured":"Winwood, S., Klein, G., Sewell, T., Andronick, J., Cock, D., Norrish, M.: Mind the gap: A verification framework for low-level C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 500\u2013515. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Formal Verification of Object-Oriented Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-18070-5_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T18:09:13Z","timestamp":1559930953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18070-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642180699","9783642180705"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18070-5_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}