{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:47:10Z","timestamp":1767926830693,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642033582","type":"print"},{"value":"9783642033599","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_34","type":"book-chapter","created":{"date-parts":[[2009,8,20]],"date-time":"2009-08-20T01:46:12Z","timestamp":1250732772000},"page":"500-515","source":"Crossref","is-referenced-by-count":29,"title":["Mind the Gap"],"prefix":"10.1007","author":[{"given":"Simon","family":"Winwood","sequence":"first","affiliation":[]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Sewell","sequence":"additional","affiliation":[]},{"given":"June","family":"Andronick","sequence":"additional","affiliation":[]},{"given":"David","family":"Cock","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"34_CR1","unstructured":"Andronick, J.: Mod\u00e9lisation et V\u00e9rification Formelles de Syst\u00e8mes Embarqu\u00e9s dans les Cartes \u00e0 Microprocesseur\u2014Plate-Forme Java Card et Syst\u00e8me d\u2019Exploitation. Ph.D thesis, Universit\u00e9 Paris-Sud (March 2006)"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/11526841_21","volume-title":"FM 2005: Formal Methods","author":"J. Andronick","year":"2005","unstructured":"Andronick, J., Chetali, B., Paulin-Mohring, C.: Formal verification of security properties of smart card embedded source code. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 302\u2013317. Springer, Heidelberg (2005)"},{"issue":"11","key":"34_CR3","doi-asserted-by":"publisher","first-page":"1382","DOI":"10.1109\/32.41331","volume":"15","author":"W.R. Bevier","year":"1989","unstructured":"Bevier, W.R.: Kit: A study in operating system verification. IEEE Transactions on Software Engineering\u00a015(11), 1382\u20131396 (1989)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"34_CR4","unstructured":"Cock, D.: Bitfields and tagged unions in C: Verification through automatic generation. In: Beckert, B., Klein, G. (eds.) Proc, 5th VERIFY, Sydney, Australia, August 2008. CEUR Workshop Proceedings, vol.\u00a0372, pp. 44\u201355 (2008)"},{"key":"34_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-71067-7_16","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Cock","year":"2008","unstructured":"Cock, D., Klein, G., Sewell, T.: Secure microkernels, state monads and scalable refinement. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 167\u2013182. Springer, Heidelberg (2008)"},{"key":"34_CR6","unstructured":"Cohen, E., Moska\u0142, M., Schulte, W., Tobies, S.: A precise yet efficient memory model for C (2008), http:\/\/research.microsoft.com\/apps\/pubs\/default.aspx?id=77174"},{"key":"34_CR7","doi-asserted-by":"crossref","unstructured":"de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science, vol.\u00a047. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511663079"},{"key":"34_CR8","doi-asserted-by":"crossref","unstructured":"Derrin, P., Elphinstone, K., Klein, G., Cock, D., Chakravarty, M.M.T.: Running the manual: An approach to high-assurance microkernel development. In: Proc. ACM SIGPLAN Haskell WS, Portland, OR, USA (September 2006)","DOI":"10.1145\/1159842.1159850"},{"issue":"8","key":"34_CR9","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E.W. Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. CACM\u00a018(8), 453\u2013457 (1975)","journal-title":"CACM"},{"key":"34_CR10","unstructured":"Elphinstone, K., Klein, G., Derrin, P., Roscoe, T., Heiser, G.: Towards a practical, verified kernel. In: Proc. 11th Workshop on Hot Topics in Operating Systems (2007)"},{"key":"34_CR11","unstructured":"Elphinstone, K., Klein, G., Kolanski, R.: Formalising a high-performance microkernel. In: Leino, R. (ed.) VSTTE, Microsoft Research Technical Report MSR-TR-2006-117, Seattle, USA, August 2006, pp. 1\u20137 (2006)"},{"key":"34_CR12","doi-asserted-by":"crossref","unstructured":"Feiertag, R.J., Neumann, P.G.: The foundations of a provably secure operating system (PSOS). In: AFIPS Conf. Proc., 1979 National Comp. Conf., New York, NY, USA, June 1979, pp. 329\u2013334 (1979)","DOI":"10.1109\/MARK.1979.8817256"},{"key":"34_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"key":"34_CR14","unstructured":"Frama-C (2008), http:\/\/frama-c.cea.fr\/"},{"key":"34_CR15","unstructured":"Hohmuth, M., Tews, H.: The VFiasco approach for a verified operating system. In: Proc. 2nd ECOOP-PLOS Workshop, Glasgow, UK (October 2005)"},{"key":"34_CR16","unstructured":"Programming languages\u2014C, ISO\/IEC 9899:1999 (1999)"},{"issue":"1","key":"34_CR17","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/s12046-009-0002-4","volume":"34","author":"G. Klein","year":"2009","unstructured":"Klein, G.: Operating system verification\u2014An overview. S\u0101dhan\u0101\u00a034(1), 27\u201369 (2009)","journal-title":"S\u0101dhan\u0101"},{"key":"34_CR18","doi-asserted-by":"crossref","unstructured":"Liedtke, J.: On \u03bc-kernel construction. In: Proc. 15th SOSP (December 1995)","DOI":"10.1145\/224056.224075"},{"key":"34_CR19","unstructured":"Moy, Y.: Union and cast in deductive verification. In: Proc. C\/C++ Verification Workshop, Technical Report ICIS-R07015. Radboud University Nijmegen (2007)"},{"key":"34_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-73595-3_27","volume-title":"Automated Deduction \u2013 CADE-21","author":"O. M\u00fcrk","year":"2007","unstructured":"M\u00fcrk, O., Larsson, D., H\u00e4hnle, R.: KeY-C: A tool for verification of C programs. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol.\u00a04603, pp. 385\u2013390. Springer, Heidelberg (2007)"},{"key":"34_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"34_CR22","unstructured":"Open Kernel Labs. OKL4 v2.1 (2008), http:\/\/www.ok-labs.com"},{"key":"34_CR23","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle\/HOL. Ph.D thesis, Technische Universit\u00e4t M\u00fcnchen (2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"issue":"2-4","key":"34_CR24","first-page":"389","volume":"42","author":"N. Schirmer","year":"2009","unstructured":"Schirmer, N., Hillebrand, M., Leinenbach, D., Alkassar, E., Starostin, A., Tsyban, A.: Balancing the load \u2014 leveraging a semantics stack for systems verification. JAR, special issue on Operating System Verification\u00a042(2-4), 389\u2013454 (2009)","journal-title":"JAR, special issue on Operating System Verification"},{"key":"34_CR25","unstructured":"Tuch, H.: Formal Memory Models for Verifying C Systems Code. Ph.D thesis, School Comp. Sci. & Engin., University NSW, Sydney 2052, Australia (August 2008)"},{"issue":"2\u20134","key":"34_CR26","first-page":"125","volume":"42","author":"H. Tuch","year":"2009","unstructured":"Tuch, H.: Formal verification of C systems code: Structured types, separation logic and theorem proving. JAR, special issue on Operating System Verification\u00a042(2\u20134), 125\u2013187 (2009)","journal-title":"JAR, special issue on Operating System Verification"},{"key":"34_CR27","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: Hofmann, M., Felleisen, M. (eds.) Proc. 34th POPL, pp. 97\u2013108. ACM, New York (2007)"},{"issue":"2","key":"34_CR28","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. CACM\u00a023(2), 118\u2013131 (1980)","journal-title":"CACM"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03359-9_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,21]],"date-time":"2020-05-21T15:18:36Z","timestamp":1590074316000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}