{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:36:26Z","timestamp":1725539786015},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642045691"},{"type":"electronic","value":"9783642045707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04570-7_12","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T04:51:23Z","timestamp":1257223883000},"page":"149-164","source":"Crossref","is-referenced-by-count":1,"title":["Preemption Abstraction"],"prefix":"10.1007","author":[{"given":"Erik","family":"Schierboom","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alejandro","family":"Tamalet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hendrik","family":"Tews","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marko","family":"van Eekelen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sjaak","family":"Smetsers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-540-87873-5_18","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E. Alkassar","year":"2008","unstructured":"Alkassar, E., Hillebrand, M.A., Leinenbach, D., Schirmer, N.W., Starostin, A.: The Verisoft approach to systems verification. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 209\u2013224. Springer, Heidelberg (2008)"},{"key":"12_CR2","unstructured":"Annamalai, S.: Verification of the Fiasco IPC implementation. Master\u2019s thesis, Dresden University of Technology (December 2005)"},{"key":"12_CR3","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":"12_CR4","unstructured":"Daum, M., D\u00f6rrenb\u00e4cher, J., Bogan, S.: Model stack for the pervasive verification of a microkernel-based operating system. In: Beckert, B., Klein, G. (eds.) 5th International Verification Workshop, CEUR Workshop Proceedings, vol.\u00a0372, pp. 56\u201370 (2008), CEUR-WS.org"},{"key":"12_CR5","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":"12_CR6","unstructured":"Endrawaty: Verification of the Fiasco IPC Implementation. Master\u2019s thesis, Dresden University of Technology (March 2005)"},{"key":"12_CR7","unstructured":"Hohmuth, M., H\u00e4rtig, H.: Pragmatic nonblocking synchronization for real-time systems. In: Proceedings of the General Track: 2002 USENIX Annual Technical Conference, Berkeley, CA, USA, pp. 217\u2013230. USENIX Association (2001)"},{"key":"12_CR8","unstructured":"Hartig, H., Hohmuth, M., Wolter, J.: Taming linux. In: Proceedings of the 5th Annual Australasian Conference on Parallel And Real-Time Systems, PART 1998 (1998)"},{"key":"12_CR9","unstructured":"Hunt, G., Larus, J.R., Abadi, M., Aiken, M., Barham, P., F\u00e4hndrich, M., Hawblitzel, C., Hodson, O., Levi, S., Murphy, N., Steensgaard, B., Tarditi, D., Wobber, T., Zill, B.D.: An overview of the Singularity project. Technical report, Microsoft Research (October 2005)"},{"key":"12_CR10","unstructured":"Hohmuth, M.: The Fiasco kernel: Requirements definition. Technical Report TUD-FI98-12, TU Dresden (1998), \n                    \n                      http:\/\/os.inf.tu-dresden.de\/fiasco\/doc.html"},{"key":"12_CR11","unstructured":"Hohmuth, M.: Pragmatic nonblocking synchronization for real-time systems. PhD thesis, TU Dresden, Fakult\u00e4t Informatik (September 2002)"},{"key":"12_CR12","unstructured":"Hohmuth, M., Peter, M.: Helping in a multiprocessor environment. In: Proceeding of the Second Workshop on Common Microkernel System Platforms (2001)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-540-77966-7_14","volume-title":"Hardware and Software: Verification and Testing","author":"M.A. Hillebrand","year":"2008","unstructured":"Hillebrand, M.A., Paul, W.J.: On the architecture of system verification environments. In: Yorav, K. (ed.) HVC 2007. LNCS, vol.\u00a04899, pp. 153\u2013168. Springer, Heidelberg (2008)"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"SPIN Model Checking and Software Verification","year":"2000","unstructured":"Havelund, K., Penix, J., Visser, W. (eds.): SPIN 2000. LNCS, vol.\u00a01885. Springer, Heidelberg (2000)"},{"key":"12_CR15","unstructured":"Hohmuth, M., Tews, H.: The VFiasco approach for a verified operating system. In: Proceedings of the 2nd ECOOP Workshop on Programming Languages and Operating Systems, Glasgow (2005)"},{"key":"12_CR16","unstructured":"Kolanski, R., Klein, G.: Formalising the L4 microkernel API. In: CATS 2006: Proceedings of the 12th Computing: The Australasian Theroy Symposium, Darlinghurst, Australia, pp. 53\u201368 (2006)"},{"issue":"1","key":"12_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":"12_CR18","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS language reference (version 2.4). Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA (November 2001)"},{"key":"12_CR19","unstructured":"Reusner, R.: Implementierung eines Echtzeit-IPC-Pfades mit Unterbre-chungspunkten f\u00fcr L4\/Fiasco. Master\u2019s thesis, TU Dresden (July 2005)"},{"key":"12_CR20","unstructured":"Schierboom, E.G.H.: Verification of the Fiasco IPC Implementation. Master\u2019s thesis, Radboud University, Computing Science Department (2007)"},{"key":"12_CR21","unstructured":"Shapiro, J., Doerrie, M., Sridhar, S., Miller, M.: Towards a verified, general-purpose operating system kernel. In: Proc. NICTA OS Verification Workshop 2004, Sydney, New South Wales, Australia (October 2004)"},{"key":"#cr-split#-12_CR22.1","unstructured":"Tews, H.: Formal Methods in the Robin project: Specification and verification of the Nova microhypervisor. In: Tews, H. (ed.) Proceedings of the C\/C++ Verification Workshop, July 2007, pp. 59???68 (2007);"},{"key":"#cr-split#-12_CR22.2","unstructured":"Technical eport ICIS-R07015, Radboud University Nijmegen"},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"Tuch, H.: Formal verification of C systems code: Structured types, separation logic and theorem proving. Journal of Automated Reasoning: Special Issue on Operating System Verification, 59 (to appear, 2009)","DOI":"10.1007\/s10817-009-9120-2"},{"issue":"2-4","key":"12_CR24","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s10817-009-9122-0","volume":"42","author":"H. Tews","year":"2009","unstructured":"Tews, H., V\u00f6lp, M., Weber, T.: Formal memory models for the verification of low-level operating-system code. Journal of Automated Reasoning\u00a042(2-4), 189\u2013227 (2009)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04570-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,10]],"date-time":"2019-03-10T10:08:41Z","timestamp":1552212521000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04570-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642045691","9783642045707"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04570-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}