{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,9]],"date-time":"2025-02-09T04:10:01Z","timestamp":1739074201256,"version":"3.37.0"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"2-4","license":[{"start":{"date-parts":[[2009,4,1]],"date-time":"2009-04-01T00:00:00Z","timestamp":1238544000000},"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-9122-0","type":"journal-article","created":{"date-parts":[[2009,4,22]],"date-time":"2009-04-22T07:32:31Z","timestamp":1240385551000},"page":"189-227","source":"Crossref","is-referenced-by-count":15,"title":["Formal Memory Models for the Verification of Low-Level Operating-System Code"],"prefix":"10.1007","volume":"42","author":[{"given":"Hendrik","family":"Tews","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcus","family":"V\u00f6lp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tjark","family":"Weber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,4,23]]},"reference":[{"key":"9122_CR1","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/978-3-540-87873-5_18","volume-title":"Verified Software: Theories, Tools, Experiments Second International Conference, VSTTE 2008, Toronto, Canada, October\u00a06\u20139, 2008, Proceedings. Lecture Notes in Computer Science, Toronto, Canada, vol. 5295","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.) Verified Software: Theories, Tools, Experiments Second International Conference, VSTTE 2008, Toronto, Canada, October\u00a06\u20139, 2008, Proceedings. Lecture Notes in Computer Science, Toronto, Canada, vol. 5295, pp. 209\u2013224. Springer, New York (2008)"},{"issue":"11","key":"9122_CR2","doi-asserted-by":"crossref","first-page":"1382","DOI":"10.1109\/32.41331","volume":"15","author":"WR Bevier","year":"1989","unstructured":"Bevier, W.R.: Kit: a study in operating system verification. IEEE Trans. Softw. Eng. 15(11), 1382\u20131396 (1989)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"4\u20135","key":"9122_CR3","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":"9122_CR4","unstructured":"Science Applications International Corporation: Green Hills Software INTEGRITY-178B Separation Kernel security target, ver.\u00a01.0 (2008). Available from http:\/\/www.niap-ccevs.org\/cc-scheme\/st\/st_vid10119-st.pdf . Retrieved February\u00a011, 2009"},{"key":"9122_CR5","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/978-3-540-87873-5_15","volume-title":"Verified Software: Theories, Tools, Experiments. Second International Conference, VSTTE 2008, Toronto, Canada, October 6\u20139, 2008, Proceedings. Lecture Notes in Computer Science, Toronto, Canada, vol. 5295","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: Woodcock, J., Shankar, N. (eds.) Verified Software: Theories, Tools, Experiments. Second International Conference, VSTTE 2008, Toronto, Canada, October 6\u20139, 2008, Proceedings. Lecture Notes in Computer Science, Toronto, Canada, vol. 5295, pp. 161\u2013176. Springer, New York (2008)"},{"key":"9122_CR6","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 (VERIFY\u201908). CEUR Workshop Proceedings, vol. 372, pp. 56\u201370. CEUR-WS.org (2008)"},{"key":"9122_CR7","doi-asserted-by":"crossref","unstructured":"Hillebrand, M., In\u00a0der Rieden, T., Paul, W.J.: Dealing with I\/O devices in the context of pervasive system verification. In: 23nd IEEE International Conference on Computer Design: VLSI in Computers and Processors (ICCD 2005), 2-5 October 2005, San Jose, CA, USA, Proceedings, pp. 309\u2013316. IEEE (2005)","DOI":"10.1109\/ICCD.2005.42"},{"key":"9122_CR8","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, Haifa, Israel, October\u00a023\u201325, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4899","author":"MA Hillebrand","year":"2008","unstructured":"Hillebrand, M.A., Paul W.J.: On the architecture of system verification environments. In: Yorav, K. (ed.) Hardware and Software: Verification and Testing, Third International Haifa Verification Conference, HVC 2007, Haifa, Israel, October\u00a023\u201325, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4899, pp. 153\u2013168. Springer, New York (2008)"},{"key":"9122_CR9","unstructured":"Hohmuth, M., Tews, H.: The semantics of C+\u2009+ data types: Towards verifying low-level system components. In: Basin, D., Wolff, B. (eds.) 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Emerging Trends Proceedings, pp. 127\u2013144. Institut f\u00fcr Informatik, Universit\u00e4t Freiburg (2003). Technical report no.\u00a0187"},{"key":"9122_CR10","unstructured":"Hohmuth, M., Tews, H.: The VFiasco approach for a verified operating system. In: 2nd ECOOP Workshop on Programming Languages and Operating Systems (ECOOP-PLOS), Glasgow, UK (2005)"},{"key":"9122_CR11","doi-asserted-by":"crossref","unstructured":"H\u00e4rtig, H., Hohmuth, M., Feske, N., Helmuth, C., Lackorzynski, A., Mehnert, F., Peter M.: The Nizza secure-system architecture. In: First International Conference on Collaborative Computing: Networking, Applications and Worksharing, San Jose, California, USA (2005)","DOI":"10.1109\/COLCOM.2005.1651218"},{"key":"9122_CR12","first-page":"284","volume-title":"Fundamental Approaches to Software Engineering. Lecture Notes in Computer Science, vol. 1783","author":"M Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) Fundamental Approaches to Software Engineering. Lecture Notes in Computer Science, vol. 1783, pp. 284\u2013303. Springer, Berlin (2000)"},{"key":"9122_CR13","unstructured":"IBM Systems: Virtualization, ver.\u00a02, release\u00a01 (2005). Available from http:\/\/publib.boulder.ibm.com\/infocenter\/eserver\/v1r2\/topic\/eicay\/eicay.pdf . Retrieved December\u00a018, 2008"},{"key":"9122_CR14","unstructured":"Intel Corporation, Denver, Colorado: Intel 64 and IA-32 Architectures Software Developer\u2019s Manual (2007). Order Number: 25366[5-9]-023US"},{"key":"9122_CR15","unstructured":"Intel Corporation: TLBs, Paging-Structure Caches, and Their Invalidation (2008). Application note 317080-002"},{"key":"9122_CR16","unstructured":"ISO\/IEC JTC1\/SC22\/WG21 C+\u2009+ Standards Committee: Programming Languages\u2014C+\u2009+ (1998). ISO\/IEC 14882:1998"},{"key":"9122_CR17","unstructured":"Klein, G.: Operating system verification\u2014an overview. Technical report NRL-955, NICTA, Sydney, Australia (2008)"},{"key":"9122_CR18","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.entcs.2008.06.042","volume":"217","author":"R Kolanski","year":"2008","unstructured":"Kolanski, R.: A logic for virtual memory. Electr. Notes Theor. Comput. Sci. 217 61\u201377 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9122_CR19","doi-asserted-by":"crossref","unstructured":"Kolanski, R., Klein, G.: Mapped separation logic. In: Woodcock, J., Shankar, N. (eds.) Proceedings of VSTTE 2008\u2014Verified Software: Theories, Tools and Experiments. Lecture Notes in Computer Science, vol. 5295, pp. 15\u201329. Toronto, Canada, Springer (2008). ISBN:978-3-540-87872-8","DOI":"10.1007\/978-3-540-87873-5_6"},{"key":"9122_CR20","unstructured":"Norrish, M.: C formalised in HOL. Technical report UCAM-CL-TR-453. Computer Laboratory, University of Cambridge (1998)"},{"key":"9122_CR21","first-page":"411","volume-title":"Computer Aided Verification. Lecture Notes in Computer Science, vol. 1102","author":"S Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 1102, pp. 411\u2013414. Springer, Berlin (1996)"},{"key":"9122_CR22","unstructured":"Robin: Open robust infrastructures. Project webpage http:\/\/robin.tudos.org (2006)"},{"key":"9122_CR23","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of sequential imperative programs in Isabelle\/HOL. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"9122_CR24","unstructured":"Tews, H.: Micro hypervisor verification: Possible approaches and relevant properties. In: NLUUG Voorjaarsconferentie 2007: Virtualisatie, pp. 96\u2013109 (2007)"},{"key":"9122_CR25","doi-asserted-by":"crossref","unstructured":"Tews, H., Weber, T., V\u00f6lp, M.: 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 the 3rd International Workshop on System Software Verification (SSV08). Electronic Notes in Theoretical Computer Science, vol. 217, pp. 79\u201396. Sydney (2008)","DOI":"10.1016\/j.entcs.2008.06.043"},{"key":"9122_CR26","unstructured":"Tews, H., Weber, T., Poll, E., van Eekelen, M., van Rossum, P.: Formal Nova interface specification. Technical report ICIS\u2013R08011, Radboud University Nijmegen (2008)"},{"key":"9122_CR27","unstructured":"Tews, H., Weber, T., V\u00f6lp, M., Poll, E., van Eekelen, M., van Rossum, P.: Nova micro\u2013hypervisor verification. Technical report ICIS\u2013R08012, Radboud University Nijmegen (2008)"},{"key":"9122_CR28","unstructured":"Tuch, H.: Formal memory models for verifying C systems code. PhD thesis, University of NSW, Sydney 2052, Australia (2008)"},{"key":"9122_CR29","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1016\/j.entcs.2008.06.041","volume":"217","author":"H Tuch","year":"2008","unstructured":"Tuch, H.: Structured types and separation logic. Electr. Notes Theor. Comput. Sci. 217, 41\u201359 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9122_CR30","doi-asserted-by":"crossref","unstructured":"Tuch, H., Klein, G.: A unified memory model for pointers. In: Sutcliffe, G., Voronkov, A. (eds.) 12th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-12). Lecture Notes in Computer Science, vol. 3835, pp. 474\u2013488. Jamaica (2005)","DOI":"10.1007\/11591191_33"},{"key":"9122_CR31","doi-asserted-by":"crossref","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) Proc. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201907), pp. 97\u2013108. Nice, France (2007)","DOI":"10.1145\/1190216.1190234"},{"key":"9122_CR32","unstructured":"VFiasco: Verified Fiasco. Project webpage http:\/\/os.inf.tu-dresden.de\/vfiasco (2001)"},{"key":"9122_CR33","unstructured":"V\u00f6lp, M., Courcambeck, S., Schwarz, C.: Final activity report. Robin project deliverable D.8, Technische Universit\u00e4t Dresden, Germany (2008)"},{"issue":"2","key":"9122_CR34","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1145\/358818.358825","volume":"23","author":"BJ Walker","year":"1980","unstructured":"Walker, B.J., Kemmerer, R.A., Popek, G.J.: Specification and verification of the UCLA Unix security kernel. Commun. ACM 23(2), 118\u2013131 (1980)","journal-title":"Commun. ACM"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9122-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9122-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9122-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,9]],"date-time":"2025-02-09T03:44:23Z","timestamp":1739072663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9122-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,4]]},"references-count":34,"journal-issue":{"issue":"2-4","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["9122"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9122-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2009,4]]}}}