{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:18:15Z","timestamp":1775053095554,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540439288","type":"print"},{"value":"9783540456148","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_6","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:45:28Z","timestamp":1179377128000},"page":"89-105","source":"Crossref","is-referenced-by-count":21,"title":["Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited"],"prefix":"10.1007","author":[{"given":"David","family":"von Oheimb","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and K. R. M. Leino. A logic of object-oriented programs. In Theory and Practice of Software Development, volume 1214 of Lect. Notes in Comp. Sci., pages 682\u2013696. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0030634"},{"key":"6_CR2","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/0890-5401(90)90037-I","volume":"84","author":"P. America","year":"1990","unstructured":"P. America and F. de Boer. Proving total correctness of recursive procedures. Information and Computation, 84:129\u2013162, 1990.","journal-title":"Information and Computation"},{"key":"6_CR3","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K. R. Apt","year":"1981","unstructured":"K. R. Apt. Ten years of Hoare logic: A survey \u2014 part I. ACM Trans. on Prog. Languages and Systems, 3:431\u2013483, 1981.","journal-title":"ACM Trans. on Prog. Languages and Systems"},{"issue":"1","key":"6_CR4","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S.A. Cook","year":"1978","unstructured":"S.A. Cook. Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing, 7(1):70\u201390, 1978.","journal-title":"SIAM Journal on Computing"},{"key":"6_CR5","unstructured":"G. A. Gorelick. A complete axiomatic system for proving assertions about recursive and non-recursive programs. Technical Report 75, Department of Computer Science, University of Toronto, 1975."},{"key":"6_CR6","unstructured":"M. Huisman. Java program verification in Higher-order logic with PVS and Isabelle. PhD thesis, University of Nijmegen, 2001."},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"M. Huisman and B. Jacobs. Java program verification via a Hoare logic with abrupt termination. In Fundamental Approaches to Software Engineering, volume 1783 of Lect. Notes in Comp. Sci., pages 284\u2013303. Springer-Verlag, 2000.","DOI":"10.1007\/3-540-46428-X_20"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"A. Igarashi, B. Pierce, and P. Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In ACM Symposium on Object Oriented Programming: Systems, Languages, and Applications (OOPSLA), Oct. 1999. Full version in ACM Transactions on Programming Languages and Systems (TOPLAS), 2001.","DOI":"10.1145\/503502.503505"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"B. Jacobs and E. Poll. A logic for the Java Modeling Language JML. In H. Hussmann, editor, Fundamental Approaches to Software Engineering, volume 2029 of Lect. Notes in Comp. Sci., pages 284\u2013299. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45314-8_21"},{"key":"6_CR10","unstructured":"T. Kleymann. Hoare logic and VDM: Machine-checked soundness and completeness proofs. Ph.D. Thesis, ECS-LFCS-98-392, LFCS, 1998."},{"key":"6_CR11","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s001650050057","volume":"11","author":"T. Kleymann","year":"1999","unstructured":"T. Kleymann. Hoare logic and auxiliary variables. Formal Aspects of Computing, 11:541\u2013566, 1999.","journal-title":"Formal Aspects of Computing"},{"key":"6_CR12","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/BF00289468","volume":"7","author":"T. Kowaltowski","year":"1977","unstructured":"T. Kowaltowski. Axiomatic approach to side effects and general jumps. Acta Informatica, 7:357\u2013360, 1977.","journal-title":"Acta Informatica"},{"key":"6_CR13","unstructured":"K. R. M. Leino. Ecstatic: An object-oriented programming language with an axiomatic semantics. In Fourth International Workshop on Foundations of Object-Oriented Programming (FOOL 4), 1997."},{"key":"6_CR14","unstructured":"J. Morris. Comments on \u201cprocedures and parameters\u201d. Undated and unpublished."},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. In V. Chandru and V. Vinay, editors, Foundations of Software Technology and Theoretical Computer Science, volume 1180 of Lect. Notes in Comp. Sci., pages 180\u2013192. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-62034-6_48"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Hoare logics for recursive procedures and unbounded nondeterminism. Draft, 2001.","DOI":"10.1007\/3-540-45793-3_8"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"T. Nipkow. Hoare logics in Isabelle\/HOL. In Proof and System-Reliability, 2002.","DOI":"10.1007\/3-540-45949-9"},{"key":"6_CR18","unstructured":"T. Nipkow, D. v. Oheimb, and C. Pusch. \u03bcJava: Embedding a programming language in a theorem prover. In F. Bauer and R. Steinbr\u00fcggen, editors, Foundations of Secure Computation, pages 117\u2013144. IOS Press, 2000. http:\/\/isabelle.in.tum.de\/Bali\/papers\/MOD99.html ."},{"key":"6_CR19","series-title":"Lect Notes Comput Sci","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":"T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. http:\/\/www4.in.tum.de\/~nipkow\/LNCS2283\/ ."},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"D. v. Oheimb. Hoare logic for mutual recursion and local variables. In C. P. Rangan, V. Raman, and R. Ramanujam, editors, Foundations of Software Technology and Theoretical Computer Science, volume 1738 of Lect. Notes in Comp. Sci., pages 168\u2013180. Springer-Verlag, 1999. http:\/\/isabelle.in.tum.de\/Bali\/papers\/FSTTCS99.html .","DOI":"10.1007\/3-540-46691-6_13"},{"key":"6_CR21","unstructured":"D. v. Oheimb. Analyzing Java in Isabelle\/HOL: Formalization, Type Safety and Hoare Logic. PhD thesis, Technische Universit\u00e4t M\u00fcnchen, 2001. http:\/\/www4.in.tum.de\/~oheimb\/diss\/ ."},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"D. v. Oheimb. Hoare logic for Java in Isabelle\/HOL. Concurrency and Computation: Practice and Experience, 13(13), 2001. http:\/\/isabelle.in.tum.de\/Bali\/papers\/CPE01.html .","DOI":"10.1002\/cpe.598"},{"key":"6_CR23","unstructured":"A. Poetzsch-Heffter. Personal communication, Aug. 2001."},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"A. Poetzsch-Heffter and P. M\u00fcller. A programming logic for sequential Java. In S. Swierstra, editor, Programming Languages and Systems (ESOP\u2019 99), volume 1576 of Lect. Notes in Comp. Sci., pages 162\u2013176. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-49099-X_11"}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T04:05:42Z","timestamp":1556424342000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}