{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T08:50:58Z","timestamp":1762505458168},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"2-4","license":[{"start":{"date-parts":[[2009,3,28]],"date-time":"2009-03-28T00:00:00Z","timestamp":1238198400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2009,4]]},"DOI":"10.1007\/s10817-009-9123-z","type":"journal-article","created":{"date-parts":[[2009,3,30]],"date-time":"2009-03-30T12:19:32Z","timestamp":1238415572000},"page":"389-454","source":"Crossref","is-referenced-by-count":29,"title":["Balancing the Load"],"prefix":"10.1007","volume":"42","author":[{"given":"Eyad","family":"Alkassar","sequence":"first","affiliation":[]},{"given":"Mark A.","family":"Hillebrand","sequence":"additional","affiliation":[]},{"given":"Dirk C.","family":"Leinenbach","sequence":"additional","affiliation":[]},{"given":"Norbert W.","family":"Schirmer","sequence":"additional","affiliation":[]},{"given":"Artem","family":"Starostin","sequence":"additional","affiliation":[]},{"given":"Alexandra","family":"Tsyban","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,3,28]]},"reference":[{"issue":"1","key":"9123_CR1","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/s12046-009-0004-2","volume":"34","author":"E Alkassar","year":"2009","unstructured":"Alkassar, E., Bogan, S., Paul, W.: Proving the correctness of client\/server software. S\u0101dhan\u0101 34(1), 145\u2013192 (2009)","journal-title":"S\u0101dhan\u0101"},{"key":"9123_CR2","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/978-3-540-87873-5_19","volume-title":"Proceedings, Verified Software: Theories, Tools, Experiments Second International Conference, VSTTE 2008. LNCS, vol.\u00a05295, Toronto, Canada, 6\u20139 October 2008","author":"E Alkassar","year":"2008","unstructured":"Alkassar, E., Hillebrand, M.A.: Formal functional verification of device drivers. In: Shankar, N., Woodcock, J. (eds.) Proceedings, Verified Software: Theories, Tools, Experiments Second International Conference, VSTTE 2008. LNCS, vol.\u00a05295, Toronto, Canada, 6\u20139 October 2008, pp.\u00a0225\u2013239. Springer, New York (2008)"},{"key":"9123_CR3","unstructured":"Alkassar, E., Hillebrand, M., Knapp, S., Rusev, R., Tverdyshev, S.: Formal device and programming model for a serial interface. In: Beckert, B. (ed.) Proceedings, 4th International Verification Workshop (VERIFY), Bremen, Germany, pp.\u00a04\u201320. CEUR-WS.org (2007)"},{"key":"9123_CR4","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/978-3-540-87873-5_18","volume-title":"Proceedings, Verified Software: Theories, Tools, Experiments Second International Conference, VSTTE 2008. LNCS, vol.\u00a05295, Toronto, Canada, 6\u20139 October 2008","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.) Proceedings, Verified Software: Theories, Tools, Experiments Second International Conference, VSTTE 2008. LNCS, vol.\u00a05295, Toronto, Canada, 6\u20139 October 2008, pp.\u00a0209\u2013224. Springer, New York (2008)"},{"key":"9123_CR5","series-title":"LNCS","first-page":"109","volume-title":"14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS08)","author":"E Alkassar","year":"2008","unstructured":"Alkassar, E., Schirmer, N., Starostin, A.: Formal pervasive verification of a paging mechanism. In: Ramakrishnan, C.R., Rehof, J. (eds.) 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS08). LNCS, vol.\u00a04963, pp.\u00a0109\u2013123. Springer, New York (2008)"},{"key":"9123_CR6","first-page":"34","volume-title":"Types for Proofs and Programs, International Workshop, TYPES 2003, Revised Selected Papers. LNCS, vol.\u00a03085, Torino, Italy, 30 April\u20134 May 2003","author":"C Ballarin","year":"2003","unstructured":"Ballarin, C.: Locales and locale expressions in Isabelle\/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) Types for Proofs and Programs, International Workshop, TYPES 2003, Revised Selected Papers. LNCS, vol.\u00a03085, Torino, Italy, 30 April\u20134 May 2003, pp.\u00a034\u201350. Springer, New York (2003)"},{"key":"9123_CR7","first-page":"31","volume-title":"Proceedings, Mathematical Knowledge Management, 5th International Conference, MKM 2006. LNCS, vol.\u00a04108, Wokingham, UK, 11\u201312 August 2006","author":"C Ballarin","year":"2006","unstructured":"Ballarin, C.: Interpretation of locales in Isabelle: theories and proof contexts. In: Borwein, J.M., Farmer, W.M. (eds.) Proceedings, Mathematical Knowledge Management, 5th International Conference, MKM 2006. LNCS, vol.\u00a04108, Wokingham, UK, 11\u201312 August 2006, pp.\u00a031\u201343. Springer, New York (2006)"},{"issue":"4","key":"9123_CR8","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/BF00243131","volume":"5","author":"WR Bevier","year":"1989","unstructured":"Bevier, W.R., Hunt, W.A., Jr., Moore, J S., Young, W.D.: An approach to systems verification. JAR 5(4), 411\u2013428 (1989)","journal-title":"JAR"},{"key":"9123_CR9","unstructured":"Beuster, G., Henrich, N., Wagner, M.: Real world verification\u2014experiences from the Verisoft email client. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) Proceedings of the FLoC\u201906 Workshop on Empirically Successful Computerized Reasoning (ESCoR 2006). CEUR Workshop Proceedings, August 2006, vol.\u00a0192, pp.\u00a0112\u2013125. CEUR-WS.org (2006)"},{"key":"9123_CR10","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/978-3-540-39724-3_7","volume-title":"Proceedings of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME)","author":"S Beyer","year":"2003","unstructured":"Beyer, S., Jacobi, C., Kroening, D., Leinenbach, D., Paul, W.: Instantiating uninterpreted functional units and memory system: functional verification of the VAMP. In: Geist, D., Tronci, E. (eds.) Proceedings of the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME). LNCS, vol.\u00a0860, pp.\u00a051\u201365. Springer, New York (2003)"},{"issue":"4\u20135","key":"9123_CR11","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/s10009-006-0204-6","volume":"8","author":"S Beyer","year":"2006","unstructured":"Beyer, S., Jacobi, C., Kroening, D., Leinenbach, D., Paul, W.: Putting it all together: formal verification of the VAMP. Int. J. Softw. Tools Technol. Transf. 8(4\u20135), 411\u2013430 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9123_CR12","unstructured":"Bogan, S.: Formal Specification of a Simple Operating System. PhD thesis, Saarland University, Computer Science Department (2008)"},{"key":"9123_CR13","first-page":"23","volume-title":"Machine Intelligence 7","author":"R Burstall","year":"1972","unstructured":"Burstall, R.: Some techniques for proving correctness of programs which alter data structures. In: Meltzer, B., Michie, D. (eds) Machine Intelligence 7, pp.\u00a023\u201350. Edinburgh University Press, Edinburgh (1972)"},{"key":"9123_CR14","unstructured":"Condea, C.: Design and implementation of a page fault handler in C0. Master\u2019s thesis, Saarland University (2006)"},{"key":"9123_CR15","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.) Proceedings, 5th International Verification Workshop (VERIFY). CEUR Workshop Proceedings, vol.\u00a0372, Sydney, Australia, August 2008, pp.\u00a056\u201370. CEUR-WS.org (2008)"},{"key":"9123_CR16","author":"M Daum","year":"2009","unstructured":"Daum, M., D\u00f6rrenb\u00e4cher, J., Wolff, B.: Proving fairness and implementation correctness of a microkernel scheduler. J. Autom. Reason. (Special Issue on Operating Systems Verification). (2009). doi: 10.1007\/s10817-009-9119-8","journal-title":"J. Autom. Reason"},{"key":"9123_CR17","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/978-3-540-87873-5_15","volume-title":"Proceedings, Verified Software: Theories, Tools, Experiments Second International Conference, VSTTE 2008. LNCS, vol.\u00a05295, Toronto, Canada, 6\u20139 October 2008","author":"M Daum","year":"2008","unstructured":"Daum, M., D\u00f6rrenb\u00e4cher, J., Wolff, B., Schmidt, M.: A verification approach for system-level concurrent programs. In: Shankar, N., Woodcock, J. (eds.) Proceedings, Verified Software: Theories, Tools, Experiments Second International Conference, VSTTE 2008. LNCS, vol.\u00a05295, Toronto, Canada, 6\u20139 October 2008, pp.\u00a0161\u2013176. Springer, New York (2008)"},{"key":"9123_CR18","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/11560548_23","volume-title":"Proceedings of the 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME 2005)","author":"I Dalinger","year":"2005","unstructured":"Dalinger, I., Hillebrand, M., Paul, W.: On the verification of memory management mechanisms. In: Borrione, D., Paul, W. (eds.) Proceedings of the 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME 2005). LNCS, vol.\u00a03725, pp.\u00a0301\u2013316. Springer, New York (2005)"},{"key":"9123_CR19","first-page":"381","volume-title":"Proceedings, Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005. LNCS, vol.\u00a03835, Montego Bay, Jamaica, 2\u20136 December 2005","author":"M Daum","year":"2005","unstructured":"Daum, M., Maus, S., Schirmer, N., Seghir, M.N.: Integration of a software model checker into Isabelle. In: Sutcliffe, G., Voronkov, A. (eds.) Proceedings, Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005. LNCS, vol.\u00a03835, Montego Bay, Jamaica, 2\u20136 December 2005, pp.\u00a0381\u2013395. Springer, New York (2005)"},{"key":"9123_CR20","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/11541868_1","volume-title":"18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005)","author":"M Gargano","year":"2005","unstructured":"Gargano, M., Hillebrand, M., Leinenbach, D., Paul, W.: On the correctness of operating system kernels. In: Hurd, J., Melham, T.F. (eds.) 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005). LNCS, vol.\u00a03603, pp.\u00a01\u201316. Springer, New York (2005)"},{"issue":"4","key":"9123_CR21","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1145\/1278901.1278904","volume":"41","author":"G Heiser","year":"2007","unstructured":"Heiser, G., Elphinstone, K., Kuz, I., Klein, G., Petters, S.M.: Towards trustworthy computing systems: taking microkernels to the next level. SIGOPS Oper. Syst. Rev. 41(4), 3\u201311 (2007)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"9123_CR22","volume-title":"Computer Architecture: A Quantitative Approach","author":"JL Hennessy","year":"1996","unstructured":"Hennessy, J.L., Patterson, D.A.: Computer Architecture: A Quantitative Approach, 2nd edn. Morgan Kaufmann, San Mateo (1996)","edition":"2"},{"key":"9123_CR23","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/978-3-540-77966-7_14","volume-title":"Hardware and Software, Verification and Testing, Third International Haifa Verification Conference, HVC 2007. LNCS, vol.\u00a04899, Haifa, Israel, 23\u201325 October 2007","author":"MA Hillebrand","year":"2008","unstructured":"Hillebrand, M.A., Paul, W.: On the architecture of system verification environments. In: Yorav, K. (ed.) Hardware and Software, Verification and Testing, Third International Haifa Verification Conference, HVC 2007. LNCS, vol.\u00a04899, Haifa, Israel, 23\u201325 October 2007, pp.\u00a0153\u2013168. Springer, New York (2008)","edition":"2007"},{"key":"9123_CR24","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"3rd Intl Workshop on Systems Software Verification (SSV 2008)","author":"T Rieden In der","year":"2008","unstructured":"In der Rieden, T., Tsyban, A.: CVM\u2014a verified framework for microkernel programmers. In: Huuck, R., Klein, G., Schlich, B. (eds.) 3rd Intl Workshop on Systems Software Verification (SSV 2008). Electronic Notes in Theoretical Computer Science, vol.\u00a0217C. Elsevier Science B.V., Oxford (2008)"},{"issue":"5","key":"9123_CR25","doi-asserted-by":"crossref","first-page":"541","DOI":"10.1007\/s001650050057","volume":"11","author":"T Kleymann","year":"1999","unstructured":"Kleymann, T.: Hoare logic and auxiliary variables. Form. Asp. Comput. 11(5), 541\u2013566 (1999)","journal-title":"Form. Asp. Comput."},{"issue":"1","key":"9123_CR26","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 34(1), 27\u201370 (2009)","journal-title":"S\u0101dhan\u0101"},{"key":"9123_CR27","unstructured":"Leinenbach, D.C.: Compiler Verification in the Context of Pervasive System Verification. PhD thesis, Saarland University, Computer Science Department (2008)"},{"key":"9123_CR28","first-page":"315","volume-title":"Computer Safety, Reliability, and Security, 26th International Conference, SAFECOMP 2007. LNCS, vol.\u00a04680, Nuremberg, Germany, 18\u201321 September 2007","author":"B Langenstein","year":"2007","unstructured":"Langenstein, B., Nonnengart, A., Rock, G., Stephan, W.: Verification of distributed applications. In: Saglietti, F., Oster, N. (eds.) Computer Safety, Reliability, and Security, 26th International Conference, SAFECOMP 2007. LNCS, vol.\u00a04680, Nuremberg, Germany, 18\u201321 September 2007, pp.\u00a0315\u2013328. Springer, New York (2007)"},{"key":"9123_CR29","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"23","volume-title":"3rd intl Workshop on Systems Software Verification (SSV 2008)","author":"D Leinenbach","year":"2008","unstructured":"Leinenbach, D., Petrova, E.: Pervasive compiler verification\u2014from verified programs to verified systems. In: Huuck, R., Klein, G., Schlich, B. (eds.) 3rd intl Workshop on Systems Software Verification (SSV 2008). Electronic Notes in Theoretical Computer Science, vol.\u00a0217C, pp.\u00a023\u201340. Elsevier Science B.V., Oxford (2008)"},{"key":"9123_CR30","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04267-0","volume-title":"Computer Architecture: Complexity and Correctness","author":"SM Mueller","year":"2000","unstructured":"Mueller, S.M., Paul, W.J.: Computer Architecture: Complexity and Correctness. Springer, New York (2000)"},{"key":"9123_CR31","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: a proof assistant for higher-order logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: a proof assistant for higher-order logic. LNCS, vol.\u00a02283. Springer, New York (2002)"},{"key":"9123_CR32","doi-asserted-by":"crossref","unstructured":"Ni, Z., Yu, D., Shao, Z.: Using XCAP to certify realistic systems code: machine context management. In: TPHOLs \u201907. LNCS, pp.\u00a0189\u2013206, Kaiserslautern, 10\u201313 September 2007","DOI":"10.1007\/978-3-540-74591-4_15"},{"key":"9123_CR33","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: a generic theorem prover","author":"LC Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: a generic theorem prover. LNCS, vol.\u00a0828. Springer, New York (1994)"},{"key":"9123_CR34","unstructured":"Petrova, E.: Verification of the C0 Compiler Implementation on the Source Code Level. PhD thesis, Saarland University, Computer Science Department (2007)"},{"key":"9123_CR35","series-title":"LNCS","first-page":"398","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004","author":"N Schirmer","year":"2005","unstructured":"Schirmer, N.: A verification environment for sequential imperative programs in Isabelle\/HOL. In: Baader, F., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004. LNCS, vol.\u00a03452, pp.\u00a0398\u2013414. Springer, New York (2005)"},{"key":"9123_CR36","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle\/HOL. PhD thesis, Technical University of Munich (2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"9123_CR37","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"169","volume-title":"3rd Intl Workshop on Systems Software Verification (SSV 2008)","author":"A Starostin","year":"2008","unstructured":"Starostin, A., Tsyban, A.: Correct microkernel primitives. In: Huuck, R., Klein, G., Schlich, B. (eds.) 3rd Intl Workshop on Systems Software Verification (SSV 2008). Electronic Notes in Theoretical Computer Science, vol.\u00a0217C, pp.\u00a0169\u2013185. Elsevier Science B.V., Oxford (2008)"},{"key":"9123_CR38","doi-asserted-by":"crossref","first-page":"240","DOI":"10.1007\/978-3-540-87873-5_20","volume-title":"Proceedings, Verified Software: Theories, Tools, Experiments Second International Conference, VSTTE 2008. LNCS, vol.\u00a05295, Toronto, Canada, 6\u20139 October 2008","author":"A Starostin","year":"2008","unstructured":"Starostin, A., Tsyban, A.: Verified process-context switch for C-programmed kernels. In: Shankar, N., Woodcock, J. (eds.) Proceedings, Verified Software: Theories, Tools, Experiments Second International Conference, VSTTE 2008. LNCS, vol.\u00a05295, Toronto, Canada, 6\u20139 October 2008, pp.\u00a0240\u2013254. Springer, New York (2008)"},{"key":"9123_CR39","first-page":"56","volume-title":"LFM 2008: Sixth NASA Langley Formal Methods Workshop, NASA Scientific and Technical Information (STI)","author":"S Tverdyshev","year":"2008","unstructured":"Tverdyshev, S., Shadrin, A.: Formal verification of gate-level computer systems. In: Rozier, K.Y. (ed.) LFM 2008: Sixth NASA Langley Formal Methods Workshop, NASA Scientific and Technical Information (STI), pp.\u00a056\u201358. NASA, Washington, DC (2008)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9123-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9123-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9123-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,17]],"date-time":"2020-05-17T04:18:53Z","timestamp":1589689133000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9123-z"}},"subtitle":["Leveraging a Semantics Stack for Systems Verification"],"short-title":[],"issued":{"date-parts":[[2009,3,28]]},"references-count":39,"journal-issue":{"issue":"2-4","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["9123"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9123-z","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,3,28]]}}}