{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:53:42Z","timestamp":1725551622330},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540305538"},{"type":"electronic","value":"9783540316503"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11591191_33","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T09:44:25Z","timestamp":1132652665000},"page":"474-488","source":"Crossref","is-referenced-by-count":12,"title":["A Unified Memory Model for Pointers"],"prefix":"10.1007","author":[{"given":"Harvey","family":"Tuch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"33_CR1","unstructured":"ARM Limited. ARM Architecture Reference Manual (June 2000)"},{"issue":"11","key":"33_CR2","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":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/10722010_8","volume-title":"Mathematics of Program Construction","author":"R. Bornat","year":"2000","unstructured":"Bornat, R.: Proving pointer programs in Hoare Logic. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 102\u2013126. Springer, Heidelberg (2000)"},{"key":"33_CR4","unstructured":"Burstall, R.: Some techniques for proving correctness of programs which alter data structures. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol.\u00a07, pp. 23\u201350. Edinburgh University Press (1972)"},{"key":"33_CR5","unstructured":"Cattel, T.: Modelization and verification of a multiprocessor realtime OS kernel. In: Proceedings of FORTE 1994, Bern, Switzerland (October 1994)"},{"key":"33_CR6","unstructured":"Duval, G., Julliand, J.: Modelling and verification of the RUBIS \u03bc-kernel with SPIN. In: SPIN 1995 Workshop Proceedings (1995)"},{"key":"33_CR7","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":"33_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11541868_1","volume-title":"Theorem Proving in Higher Order Logics","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. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 1\u201316. Springer, Heidelberg (2005)"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Hohmuth, M., Tews, H., Stephens, S.G.: Applying source-code verification to a microkernel \u2014 the VFiasco project. Technical Report TUD-FI02-03-M\u00e4rz, TU Dresden (2002)","DOI":"10.1145\/1133373.1133405"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Jensen, J., Joergensen, M., Klarlund, N., Schwartzbach, M.: Automatic verification of pointer programs using monadic second-order logic. In: PLDI 1997 (1997)","DOI":"10.1145\/258915.258936"},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Klein","year":"2004","unstructured":"Klein, G., Tuch, H.: Towards verified virtual memory in L4. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223. Springer, Heidelberg (2004)"},{"key":"33_CR12","unstructured":"L4 eXperimental Kernel Reference Manual Version X.2 (2004), http:\/\/l4hq.org\/docs\/manuals\/"},{"key":"33_CR13","doi-asserted-by":"crossref","unstructured":"Liedtke, J.: On \u03bc-kernel construction. In: 15th ACM Symposium on Operating System Principles (SOSP) (December 1995)","DOI":"10.1145\/224056.224075"},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. Information and Computation (2005) (To appear)","DOI":"10.1016\/j.ic.2004.10.007"},{"issue":"3","key":"33_CR15","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1145\/1065887.1065892","volume":"27","author":"G. Necula","year":"2005","unstructured":"Necula, G., Condit, J., Harren, M., McPeak, S., Weimer, W.: Ccured: type-safe retrofitting of legacy software. ACM Trans. Prog. Lang. Syst.\u00a027(3), 477\u2013526 (2005)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"33_CR16","unstructured":"Neumann, P.G., Boyer, R.S., Feiertag, R.J., Levitt, K.N., Robinson, L.: A provably secure operating system: The system, its applications, and proofs. Technical Report CSL-116, SRI International (1980)"},{"key":"33_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"33_CR18","unstructured":"Norrish, M.: C formalised in HOL. PhD thesis, Computer Laboratory, University of Cambridge (1998)"},{"key":"33_CR19","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. 17th IEEE Symposium on Logic in Computer Science, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"33_CR20","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-540-32275-7_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"N. Schirmer","year":"2005","unstructured":"Schirmer, N.: A verification environment for sequential imperative programs in Isabelle\/HOL. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 398\u2013414. Springer, Heidelberg (2005)"},{"key":"33_CR21","unstructured":"System Architecture Group. The L4Ka:Pistachio microkernel. White paper, University of Karlsruhe (May 2003)"},{"key":"33_CR22","unstructured":"Tuch, H., Klein, G.: Verifying the L4 virtual memory subsystem. In: Proc. NICTA FM Workshop on OS Verification, pp. 73\u201397. Technical Report 0401005T-1, National ICT Australia (2004)"},{"key":"33_CR23","doi-asserted-by":"crossref","unstructured":"Tullmann, P., Turner, J., McCorquodale, J., Lepreau, J., Chitturi, A., Back, G.: Formal methods: a practical tool for OS implementors. In: Proceedings of the Sixth Workshop on Hot Topics in Operating Systems, pp. 20\u201325 (1997)","DOI":"10.1109\/HOTOS.1997.595176"},{"issue":"2","key":"33_CR24","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. Communications of the ACM\u00a023(2), 118\u2013131 (1980)","journal-title":"Communications of the ACM"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11591191_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:02:29Z","timestamp":1605643349000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11591191_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540305538","9783540316503"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/11591191_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}