{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T05:01:22Z","timestamp":1768280482789,"version":"3.49.0"},"publisher-location":"Boston, MA","reference-count":23,"publisher":"Springer US","isbn-type":[{"value":"9781441915382","type":"print"},{"value":"9781441915399","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-1-4419-1539-9_11","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T00:26:11Z","timestamp":1267489571000},"page":"323-339","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Refinement in the Formal Verification of the seL4 Microkernel"],"prefix":"10.1007","author":[{"given":"Gerwin","family":"Klein","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Sewell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Winwood","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,1,23]]},"reference":[{"issue":"2\u20134","key":"11_CR1_11","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, Leinenbach D, Schirmer N, Starostin A, Tsyban A (2009) Balancing the load \u2013 leveraging a semantics stack for systems verification. J Autom Reason 42(2\u20134): 389\u2013454","journal-title":"J Autom Reason"},{"issue":"11","key":"11_CR2_11","doi-asserted-by":"publisher","first-page":"1382","DOI":"10.1109\/32.41331","volume":"15","author":"WR Bevier","year":"1989","unstructured":"Bevier WR (1989) Kit: a study in operating system verification. IEEE Trans Softw Eng 15(11):1382\u20131396","journal-title":"IEEE Trans Softw Eng"},{"key":"11_CR3_11","unstructured":"Cock D (2008) Bitfields and tagged unions in C: verification through automatic generation. In: Beckert B, Klein G (eds) VERIFY\u201908, vol 372 of CEUR workshop proceedings, Aug 2008, pp 44\u201355"},{"key":"11_CR4_11","series-title":"of LNCS","first-page":"167","volume-title":"21st TPHOLs","author":"D Cock","year":"2008","unstructured":"Cock D, Klein G, Sewell T (2008) Secure microkernels, state monads and scalable refinement. In: Mohamed OA, Mu\u00f1oz C, Tahar S (eds) 21st TPHOLs, vol 5170 of LNCS. Springer, Berlin, pp 167\u2013182"},{"key":"11_CR5_11","series-title":"Lecture notes in computer science Munich, Germany","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem proving in higher order logics (TPHOLs 2009)","author":"E Cohen","year":"2009","unstructured":"Cohen E, Dahlweid M, Hillebrand M, Leinenbach D, Moskal M, Santen T, Schulte W, Tobies S (2009) VCC: a practical system for verifying concurrent C. In: Theorem proving in higher order logics (TPHOLs 2009), vol 5674 of Lecture notes in computer science, Munich, Germany. Springer, Berlin, pp 23\u201342"},{"key":"11_CR6_11","doi-asserted-by":"crossref","unstructured":"de Roever W-P, Engelhardt K (1998) Data refinement: model-oriented proof methods and their comparison. In: Cambridge tracts in theoretical computer science, vol 47. Cambridge University Press, Cambridge","DOI":"10.1017\/CBO9780511663079"},{"issue":"8","key":"11_CR7_11","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra EW (1975) Guarded commands, nondeterminacy and formal derivation of programs. Commun ACM 18(8):453\u2013457","journal-title":"Commun ACM"},{"key":"11_CR8_11","unstructured":"Elphinstone K, Klein G, Derrin P, Roscoe T, Heiser G (2007) Towards a practical, verified kernel. In: Proceedings of 11th workshop on hot topics in operating systems, San Diego, CA, USA, pp 117\u2013122"},{"key":"11_CR9_11","doi-asserted-by":"crossref","unstructured":"Feiertag RJ, Neumann PG (1979) The foundations of a provably secure operating system (PSOS). In: AFIPS conference proceedings, 1979 National computer conference, New York, NY, USA, June 1979, pp 329\u2013334","DOI":"10.1109\/MARK.1979.8817256"},{"key":"11_CR10_11","unstructured":"Green Hills Software, Inc. (2008) INTEGRITY-178B separation kernel security target version 1.0. http:\/\/www.niap-ccevs.org\/cc-scheme\/st\/st_vid10119-st.pdf"},{"key":"11_CR11_11","unstructured":"Green Hills Software, Inc. (2008) Integrity real-time operating system. http:\/\/www.ghs.com\/products\/rtos\/integrity.html"},{"key":"11_CR12_11","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1145\/1180405.1180448","volume-title":"CCS \u201906: proceedings of 13th conference on computer and communications security","author":"CL Heitmeyer","year":"2006","unstructured":"Heitmeyer CL, Archer M, Leonard EI, McLean J (2006) Formal specification and verification of data separation in a separation kernel for an embedded system. In: CCS \u201906: proceedings of 13th conference on computer and communications security. ACM, New York, NY, pp 346\u2013355"},{"key":"11_CR13_11","unstructured":"Hohmuth M, Tews H (2005) The VFiasco approach for a verified operating system. In: 2nd PLOS, July 2005"},{"key":"11_CR14_11","unstructured":"Information Assurance Directorate (2007) U.S. government protection profile for separation kernels in environments requiring high robustness, June 2007. Version 1.03. http:\/\/www.niap-ccevs.org\/cc-scheme\/pp\/pp.cfm\/id\/pp_skpp_hr_v1.03\/"},{"key":"11_CR15_11","unstructured":"ISO\/IEC (2005) Programming languages \u2013 C. In: Technical report 9899:TC2, ISO\/IEC JTC1\/SC22\/WG14, May 2005"},{"issue":"1","key":"11_CR16_11","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/s12046-009-0002-4","volume":"34","author":"G Klein","year":"2009","unstructured":"Klein G (2009). Operating system verification \u2013 an overview. S\u0101dhan\u0101 34(1):27\u201369","journal-title":"S\u0101dhan\u0101"},{"key":"11_CR17_11","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 (2009) seL4: Formal verification of an OS kernel. In: Proceedings of 22th SOSP, Big Sky, MT, USA, October 2009. ACM, New York, NY, pp 207\u2013220","DOI":"10.1145\/1629575.1629596"},{"key":"11_CR18_11","doi-asserted-by":"crossref","unstructured":"Schirmer N (2006) Verification of sequential imperative programs in Isabelle\/HOL. PhD thesis, Technische Universit\u00e4t M\u00fcnchen","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"11_CR19_11","series-title":"of ENTCS","first-page":"79","volume-title":"Proceedings of 3rd international workshop on systems software verification (SSV\u201908)","author":"H Tews","year":"2008","unstructured":"Tews H, Weber T, V\u00f6lp M (2008) A formal model of memory peculiarities for the verification of low-level operating-system code. In: Huuck R, Klein G, Schlich B (eds) Proceedings of 3rd international workshop on systems software verification (SSV\u201908), vol 217 of ENTCS. Elsevier, Amsterdam, pp 79\u201396"},{"issue":"2\u20134","key":"11_CR20_11","first-page":"125","volume":"42","author":"H Tuch","year":"2009","unstructured":"Tuch H (2009) Formal verification of C systems code: structured types, separation logic and theorem proving. J Autom Reason (special issue on operating system verification) 42(2\u20134):125\u2013187","journal-title":"J Autom Reason (special issue on operating system verification)"},{"key":"11_CR21_11","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/1190216.1190234","volume-title":"Proceedings of 34th ACM SIGPLAN-SIGACT symposium on principles of programming languages, Nice","author":"H Tuch","year":"2007","unstructured":"Tuch H, Klein G, Norrish M (2007) Types, bytes, and separation logic. In: Hofmann M, Felleisen M (eds) Proceedings of 34th ACM SIGPLAN-SIGACT symposium on principles of programming languages, Nice, France. ACM, New York, NY, pp 97\u2013108"},{"issue":"2","key":"11_CR22_11","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 (1980) Specification and verification of the UCLA unix security kernel. Commun ACM 23(2):118\u2013131","journal-title":"Commun ACM"},{"key":"11_CR23_11","series-title":"of LNCS, Munich, Germany, August 2009","first-page":"500","volume-title":"Proceedings of TPHOls\u201909","author":"S Winwood","year":"2009","unstructured":"Winwood S, Klein G, Sewell T, Andronick J, Cock D, Norrish M (2009) Mind the gap: a verification framework for low-level C. In: Berghofer S, Nipkow T, Urban C, Wenzel M (eds) Proceedings of TPHOls\u201909, vol 5674 of LNCS, Munich, Germany, August 2009. Springer, Berlin, pp 500\u2013515"}],"container-title":["Design and Verification of Microprocessor Systems for High-Assurance Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4419-1539-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,5]],"date-time":"2024-08-05T17:04:51Z","timestamp":1722877491000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-1-4419-1539-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9781441915382","9781441915399"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-1-4419-1539-9_11","relation":{},"subject":[],"published":{"date-parts":[[2010]]},"assertion":[{"value":"23 January 2010","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}