{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T19:51:36Z","timestamp":1770753096034,"version":"3.50.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540252368","type":"print"},{"value":"9783540322757","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32275-7_26","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T16:14:41Z","timestamp":1292861681000},"page":"398-414","source":"Crossref","is-referenced-by-count":88,"title":["A Verification Environment for Sequential Imperative Programs in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Norbert","family":"Schirmer","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"26_CR2","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. 23\u201350. Edinburgh University Press, Edinburgh (1972)"},{"issue":"4","key":"26_CR3","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1017\/S095679680200446X","volume":"13","author":"J.-C. Filli\u00e2tre","year":"2003","unstructured":"Filli\u00e2tre, J.-C.: Verification of Non-Functional Programs using Interpretations in Type Theory. Journal of Functional Programming\u00a013(4), 709\u2013745 (2003)","journal-title":"Journal of Functional Programming"},{"key":"26_CR4","unstructured":"Filli\u00e2tre, J.-C.: Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Universit\u00e9 Paris Sud (March 2003)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/BFb0055136","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1998","unstructured":"Harrison, J.: Formalizing Dijkstra. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 171\u2013188. Springer, Heidelberg (1998)"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Homeier, P.V.: Trustworthy Tools for Trustworthy Programs: A Mechanically Verified Verification Condition Generator for the Total Correctness of Procedures. PhD thesis, Department of Computer Science, University of California, Los Angeles (1995)","DOI":"10.1007\/3-540-58450-1_48"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Huisman, M.: Java program verification in higher order logic with PVS and Isabelle. PhD thesis, University of Nijmegen (2000)","DOI":"10.1007\/3-540-46428-X_20"},{"key":"26_CR8","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.jlap.2003.07.005","volume":"58","author":"B. Jacobs","year":"2004","unstructured":"Jacobs, B.: Weakest precondition reasoning for Java programs with JML annotations. Journal of Logic and Algebraic Programming\u00a058, 61\u201388 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"issue":"5","key":"26_CR9","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s001650050057","volume":"11","author":"T. Kleymann","year":"1999","unstructured":"Kleymann, T.: Hoare Logic and auxiliary variables. Formal Aspects of Computing\u00a011(5), 541\u2013566 (1999)","journal-title":"Formal Aspects of Computing"},{"key":"26_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-45085-6_10","volume-title":"Automated Deduction \u2013 CADE-19","author":"F. Mehta","year":"2003","unstructured":"Mehta, F., Nipkow, T.: Proving pointer programs in higher-order logic. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 121\u2013135. Springer, Heidelberg (2003)"},{"key":"26_CR11","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"},{"key":"26_CR12","first-page":"387","volume-title":"Current Trends in Hardware Verification and Automatic Theorem Proving (Proceedings of the Workshop on Hardware Verification)","author":"M.J.C. Gordon","year":"1988","unstructured":"Gordon, M.J.C.: Mechanizing programming logics in higher-order logic. In: Birtwistle, G.M., Subrahmanyam, P.A. (eds.) Current Trends in Hardware Verification and Automatic Theorem Proving (Proceedings of the Workshop on Hardware Verification), Banff, Canada, pp. 387\u2013439. Springer, Berlin (1988)"},{"key":"26_CR13","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-94-010-0413-8_11","volume-title":"Proof and System-Reliability","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T.: Hoare logics in Isabelle\/HOL. In: Schwichtenberg, H., Steinbr\u00fcggen, R. (eds.) Proof and System-Reliability, pp. 341\u2013367. Kluwer, Dordrecht (2002)"},{"key":"26_CR14","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.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"26_CR15","unstructured":"Norrish, M.: C formalised in HOL. PhD thesis, University of Cambridge (1998)"},{"key":"26_CR16","unstructured":"Oheimb, D.v.: Analyzing Java in Isabelle\/HOL: Formalization, Type Safety and Hoare Logic. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2001)"},{"key":"26_CR17","unstructured":"Ortner, V.: Verification of BDD Algorithms. Master\u2019s thesis, Technische Universit\u00e4t M\u00fcnchen (2004), http:\/\/www.veronika.langlotz.info\/"},{"key":"26_CR18","unstructured":"Prensa Nieto, L.: Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle\/HOL. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2002)"},{"key":"26_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 (LICS 2002), pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"26_CR20","unstructured":"Schirmer, N.: A Verification Environment for Sequential Imperative Programs in Isabelle\/HOL. In: Klein, G. (ed.) Proc. NICTA Workshop on OS Verification 2004 (2004) ID: 0401005T-1, http:\/\/www4.in.tum.de\/schirmer"},{"key":"26_CR21","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/BF01383984","volume":"3","author":"J. Wright von","year":"1993","unstructured":"von Wright, J., Hekanaho, J., Luostarinen, P., L\u00e5ngbacka, T.: Mechanizing some advanced refinement concepts. Formal Methods in System Design\u00a03, 49\u201381 (1993)","journal-title":"Formal Methods in System Design"},{"key":"26_CR22","doi-asserted-by":"crossref","unstructured":"Wadler, P.: The essence of functional programming. In: Proc. 19th ACM Symp. Principles of Programming Languages (1992)","DOI":"10.1145\/143165.143169"},{"key":"26_CR23","unstructured":"Wenzel, M.: Miscellaneous Isabelle\/Isar examples for higher order logic. Isabelle\/ Isar proof document (2001)"},{"key":"26_CR24","unstructured":"Wenzel, M.: Isabelle\/Isar \u2014 A Versatile Environment for Human-Readable Formal Proof Documents. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2002), http:\/\/tumb1.biblio.tu-muenchen.de\/publ\/diss\/in\/2002\/wenzel.html"}],"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\/978-3-540-32275-7_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:35:12Z","timestamp":1605742512000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32275-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540252368","9783540322757"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32275-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}