{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214165},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439318"},{"type":"electronic","value":"9783540456209"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45620-1_5","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T07:18:26Z","timestamp":1186903106000},"page":"63-77","source":"Crossref","is-referenced-by-count":32,"title":["Formal Verification of a Java Compiler in Isabelle"],"prefix":"10.1007","author":[{"given":"Martin","family":"Strecker","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,4]]},"reference":[{"key":"5_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Proc. TYPES Working Group Annual Meeting 2000","author":"S. Berghofer","year":"2000","unstructured":"Stefan Berghofer and Tobias Nipkow. Executing higher order logic. In Proc. TYPES Working Group Annual Meeting 2000, LNCS, 2000. Available from http:\/\/www4.in.tum.de\/~berghofe\/papers\/TYPES2000.pdf ."},{"key":"5_CR2","unstructured":"Samuel Boutin. Preuve de correction de la compilation de Mini-ML en code CAM dans le syst\u00e8me d\u2019aide \u00e0 la d\u00e9monstration COQ. Technical Report 2536, INRIA Rocquencourt, April 1995."},{"key":"5_CR3","unstructured":"Paul Curzon. A verified Vista implementation. Technical Report 311, University of Cambridge, Computer Laboratory, September 1993. Available from http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/vista\/ ."},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"A. Dold and V. Vialard. A mechanically verified compiling specification for a Lisp compiler. In Proc. FSTTCS 2001, December 2001.","DOI":"10.1007\/3-540-45294-X_13"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Gerwin Klein and Tobias Nipkow. Verified bytecode verifiers. Theoretical Computer Science, 2002. to appear.","DOI":"10.1016\/S0304-3975(02)00869-1"},{"key":"5_CR6","unstructured":"J.S. Moore, W.R. Bevier, W. A. Hunt, and W. D. Young. System verification. Special issue of J. of Automated Reasoning, 5(4), 1989."},{"key":"5_CR7","first-page":"51","volume":"7","author":"R. Milner","year":"1972","unstructured":"R. Milner and R. Weyhrauch. Proving compiler correctness in a mechanized logic. Machine Intelligence, 7:51\u201370, 1972.","journal-title":"Machine Intelligence"},{"key":"5_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45315-6_23","volume-title":"Foundations of Software Science and Computation Structures (FOS-SACS 2001)","author":"T. Nipkow","year":"2001","unstructured":"Tobias Nipkow. Verified bytecode verifiers. In M. Miculan F. Honsell, editor, Foundations of Software Science and Computation Structures (FOS-SACS 2001), volume 2030 of Lecture Notes in Computer Science. Springer Verlag, 2001."},{"key":"5_CR9","unstructured":"Tobias Nipkow, David von Oheimb, and Cornelia Pusch. \u03bcJava: Embedding a programming language in a theorem prover. In F.L. Bauer and R. Steinbr\u00fcggen, editors, Foundations of Secure Computation. Proc. Int. Summer School Marktoberdorf 1999, pages 117\u2013144. IOS Press, 2000."},{"key":"5_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL. A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle\/HOL. A Proof Assistant for Higher-Order Logic. LNCS 2283. Springer, 2002."},{"key":"5_CR11","unstructured":"David von 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":"5_CR12","doi-asserted-by":"crossref","unstructured":"David von Oheimb. Hoare logic for Java in Isabelle\/HOL. Concurrency: Practice and Experience, 13(13), 2001.","DOI":"10.1002\/cpe.598"},{"key":"5_CR13","unstructured":"G. Schellhorn. Verifikation abstrakter Zustandsmaschinen. PhD thesis, Universit\u00e4t Ulm, 1999."},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"R. St\u00e4rk, J. Schmid, and E. B\u00f6rger. Java and the Java Virtual Machine-Definition, Verification, Validation. Springer Verlag, 2001.","DOI":"10.1007\/978-3-642-59495-3"},{"key":"5_CR15","unstructured":"Martin Strecker. Compilation and bytecode verification in \u03bcJava. Forthcoming, preprint available from http:\/\/www4.in.tum.de\/~streckem\/Publications\/compbcv02.html , 2002."},{"issue":"4","key":"5_CR16","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/BF00243134","volume":"5","author":"W. D. Young","year":"1989","unstructured":"William D. Young. A mechanically verified code generator. J. of Automated Reasoning, 5(4):493\u2013518, 1989.","journal-title":"J. of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-18"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45620-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T23:56:25Z","timestamp":1556754985000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45620-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439318","9783540456209"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45620-1_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}