{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T13:04:30Z","timestamp":1762866270197,"version":"build-2065373602"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642412011"},{"type":"electronic","value":"9783642412028"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41202-8_6","type":"book-chapter","created":{"date-parts":[[2013,10,21]],"date-time":"2013-10-21T05:11:19Z","timestamp":1382332279000},"page":"70-85","source":"Crossref","is-referenced-by-count":8,"title":["Formally Verified System Initialisation"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Boyton","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"June","family":"Andronick","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Callum","family":"Bannister","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"Fernandez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xin","family":"Gao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Greenaway","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Corey","family":"Lewis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Sewell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_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":"6_CR2","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1145\/1266840.1266854","volume-title":"SACMAT","author":"B. Hicks","year":"2007","unstructured":"Hicks, B., Rueda, S., Clair, L.S., Jaeger, T., McDaniel, P.D.: A logical specification and analysis for SELinux MLS policy. In: Lotz, V., Thuraisingham, B.M. (eds.) SACMAT, pp. 91\u2013100. ACM Press, New York (2007)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-17164-2_3","volume-title":"Programming Languages and Systems","author":"G. Klein","year":"2010","unstructured":"Klein, G.: From a verified kernel towards verified systems. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol.\u00a06461, pp. 21\u201333. Springer, Heidelberg (2010)"},{"key":"6_CR4","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: 22nd SOSP, pp. 207\u2013220. ACM (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-642-32347-8_22","volume-title":"Interactive Theorem Proving","author":"G. Klein","year":"2012","unstructured":"Klein, G., Kolanski, R., Boyton, A.: Mechanised separation algebra. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 332\u2013337. Springer, Heidelberg (2012)"},{"key":"6_CR6","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, pp. 31\u201336 (August 2010)","DOI":"10.1145\/1851276.1851284"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Murray, T., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., Klein, G.: seL4: from general purpose to a proof of information flow enforcement. In: IEEE Symp. Security & Privacy, Oakland, CA (May 2013)","DOI":"10.1109\/SP.2013.35"},{"key":"6_CR8","unstructured":"National Security Agency. U.S. government protection profile for separation kernels in environments requiring high robustness, version 1.3 (June 2007)"},{"key":"6_CR9","unstructured":"Open Kernel Labs. OKL4 microkernel, reference manual (September 2008), http:\/\/wiki.ok-labs.com\/downloads\/release-3.0\/okl4-ref-manual-3.0.pdf"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. 17th IEEE Symposium on Logic in Computer Science, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Sewell, T., Myreen, M., Klein, G.: Translation validation for a verified OS kernel. In: Proc. 34th PLDI, pp. 471\u2013481. ACM (June 2013)","DOI":"10.1145\/2491956.2462183"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-642-22863-6_24","volume-title":"Interactive Theorem Proving","author":"T. Sewell","year":"2011","unstructured":"Sewell, T., Winwood, S., Gammie, P., Murray, T., Andronick, J., Klein, G.: seL4 enforces integrity. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 325\u2013340. Springer, Heidelberg (2011)"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Shapiro, J.S., Weber, S.: Verifying the EROS confinement mechanism. In: IEEE Symposium on Security and Privacy, pp. 166\u2013176. IEEE Computer Society (2000)","DOI":"10.1109\/SECPRI.2000.848454"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41202-8_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T17:42:45Z","timestamp":1746034965000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41202-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642412011","9783642412028"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41202-8_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}