{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:50:19Z","timestamp":1773654619249,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540878728","type":"print"},{"value":"9783540878735","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-87873-5_18","type":"book-chapter","created":{"date-parts":[[2008,9,25]],"date-time":"2008-09-25T12:04:10Z","timestamp":1222344250000},"page":"209-224","source":"Crossref","is-referenced-by-count":35,"title":["The Verisoft Approach to Systems Verification"],"prefix":"10.1007","author":[{"given":"Eyad","family":"Alkassar","sequence":"first","affiliation":[]},{"given":"Mark A.","family":"Hillebrand","sequence":"additional","affiliation":[]},{"given":"Dirk","family":"Leinenbach","sequence":"additional","affiliation":[]},{"given":"Norbert W.","family":"Schirmer","sequence":"additional","affiliation":[]},{"given":"Artem","family":"Starostin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"18_CR1","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/BF00243131","volume":"5","author":"W.R. Bevier","year":"1989","unstructured":"Bevier, W.R., Hunt Jr., W.A., Moore, J S., Young, W.D.: An approach to systems verification. Journal of Automated Reasoning\u00a05(4), 411\u2013428 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/978-3-540-40007-3_11","volume-title":"Formal Methods at the Crossroads. From Panacea to Foundational Support","author":"J.S. Moore","year":"2003","unstructured":"Moore, J S.: A grand challenge proposal for formal methods: A verified stack. In: Aichernig, B.K., Maibaum, T.S.E. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol.\u00a02757, pp. 161\u2013172. Springer, Heidelberg (2003)"},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1109\/CSAC.2003.1254326","volume-title":"19th Annual Computer Security Applications Conference (ACSA 2003), Las Vegas, NV, USA","author":"P.G. Neumann","year":"2003","unstructured":"Neumann, P.G., Feiertag, R.J.: PSOS Revisited. In: 19th Annual Computer Security Applications Conference (ACSA 2003), Las Vegas, NV, USA, pp. 208\u2013216. IEEE Computer Society, Los Alamitos (2003), http:\/\/csdl.computer.org\/comp\/proceedings\/acsac\/2003\/2041\/00\/20410208abs.htm"},{"issue":"2","key":"18_CR4","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1145\/358818.358825","volume":"23","author":"B.J. Walker","year":"1980","unstructured":"Walker, B.J., Kemmerer, R.A., Popek, G.J.: Specification and verification of the UCLA Unix security kernel. Comm. ACM\u00a023(2), 118\u2013131 (1980)","journal-title":"Comm. ACM"},{"issue":"4","key":"18_CR5","doi-asserted-by":"publisher","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.\u00a041(4), 3\u201311 (2007)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"18_CR6","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/1190216.1190234","volume-title":"POPL 2007","author":"H. Tuch","year":"2007","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: POPL 2007, pp. 97\u2013108. ACM Press, New York (2007)"},{"key":"18_CR7","unstructured":"Tuch, H., Klein, G.: Verifying the L4 virtual memory subsystem. In: Proc. NICTA Formal Methods Workshop on Operating Systems Verification, pp. 73\u201397 (2004)"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle\/HOL. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (April 2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-540-74591-4_15","volume-title":"Theorem Proving in Higher Order Logics","author":"Z. Ni","year":"2007","unstructured":"Ni, Z., Yu, D., Shao, Z.: Using XCAP to certify realistic systems code: Machine context management. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 189\u2013206. Springer, Heidelberg (2007)"},{"key":"18_CR10","first-page":"165","volume-title":"SIGOPS 2002","author":"M. Hohmuth","year":"2002","unstructured":"Hohmuth, M., Tews, H., Stephens, S.G.: Applying source-code verification to a microkernel: The VFiasco project. In: SIGOPS 2002, pp. 165\u2013169. ACM Press, New York (2002)"},{"key":"18_CR11","unstructured":"Tverdyshev, S., Shadrin, A.: Formal verification of gate-level computer systems. In: Rozier, K.Y. (ed.) LFM 2008. NASA STI, NASA, pp. 56\u201358 (2008)"},{"key":"18_CR12","unstructured":"Burstall, R.: Some techniques for proving correctness of programs which alter data structures. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence 7, pp. 23\u201350. Edinburgh University Press (1972)"},{"key":"18_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/11591191_27","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","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.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 381\u2013395. Springer, Heidelberg (2005)"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/978-3-540-24849-1_3","volume-title":"Types for Proofs and Programs","author":"C. Ballarin","year":"2004","unstructured":"Ballarin, C.: Locales and locale expressions in Isabelle\/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol.\u00a03085, pp. 34\u201350. Springer, Heidelberg (2004)"},{"key":"18_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11812289_4","volume-title":"Mathematical Knowledge Management","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.) MKM 2006. LNCS (LNAI), vol.\u00a04108, pp. 31\u201343. Springer, Heidelberg (2006)"},{"key":"18_CR16","unstructured":"Petrova, E.: Verification of the C0 Compiler Implementation on the Source Code Level. PhD thesis, Saarland University, Computer Science Department (2007)"},{"key":"18_CR17","unstructured":"Leinenbach, D.: Compiler Verification in the Context of Pervasive System Verification. PhD thesis, Saarland University, Computer Science Department (2008)"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","volume-title":"VSTTE 2008","author":"E. Alkassar","year":"2008","unstructured":"Alkassar, E., Hillebrand, M.A.: Formal functional verification of device drivers. In: Woodcock, J., Shankar, N. (eds.) VSTTE 2008. LNCS. Springer, Heidelberg (2008)"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-540-78800-3_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","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.) TACAS 2008. LNCS, vol.\u00a04963, pp. 109\u2013123. Springer, Heidelberg (2008)"},{"key":"18_CR20","first-page":"164","volume-title":"TIME 2008","author":"S. Tverdyshev","year":"2008","unstructured":"Tverdyshev, S., Alkassar, E.: Efficient bit-level model reductions for automated hardware verification. In: TIME 2008, pp. 164\u2013172. IEEE Computer Society Press, Los Alamitos (2008)"},{"key":"18_CR21","unstructured":"Wenzel, M.: Isabelle\/Isar \u2014 A Versatile Environment for Human-Readable Formal Proof Documents. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2002)"},{"key":"18_CR22","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., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87873-5_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:07:06Z","timestamp":1606183626000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-87873-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540878728","9783540878735"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87873-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}