{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T16:55:21Z","timestamp":1743008121436,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642041662"},{"type":"electronic","value":"9783642041679"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04167-9_7","type":"book-chapter","created":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T06:45:02Z","timestamp":1250664302000},"page":"119-138","source":"Crossref","is-referenced-by-count":1,"title":["Towards Demonstrably Correct Compilation of Java Byte Code"],"prefix":"10.1007","author":[{"given":"Michael","family":"Leuschel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.S.A. Pnueli","year":"1998","unstructured":"Pnueli, E.S.A., Siegel, M.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, p. 151. Springer, Heidelberg (1998)"},{"key":"7_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)"},{"key":"7_CR3","first-page":"343","volume-title":"On the Construction of Programs: An Advanced Course","author":"J.-R. Abrial","year":"1980","unstructured":"Abrial, J.-R., Schuman, S.A., Meyer, B.: Specification language. In: McKeag, R.M., Macnaghten, A.M. (eds.) On the Construction of Programs: An Advanced Course, pp. 343\u2013410. Cambridge University Press, Cambridge (1980)"},{"key":"7_CR4","volume-title":"Compilers. Principles, Techniques, and Tools","author":"A.V. Aho","year":"2007","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers. Principles, Techniques, and Tools, 2nd edn. Addison-Wesley, Reading (2007)","edition":"2"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-540-71316-6_12","volume-title":"Programming Languages and Systems","author":"E. Albert","year":"2007","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of java bytecode. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 157\u2013172. Springer, Heidelberg (2007)"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1145\/1296907.1296922","volume-title":"ISMM","author":"E. Albert","year":"2007","unstructured":"Albert, E., Genaim, S., G\u00f3mez-Zamalloa, M.: Heap space analysis for java bytecode. In: Morrisett, G., Sagiv, M. (eds.) ISMM, pp. 105\u2013116. ACM Press, New York (2007)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-69611-7_8","volume-title":"Practical Aspects of Declarative Languages","author":"E. Albert","year":"2006","unstructured":"Albert, E., G\u00f3mez-Zamalloa, M., Hubert, L., Puebla, G.: Verification of java bytecode using analysis and transformation of logic programs. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 124\u2013139. Springer, Heidelberg (2006)"},{"issue":"6A","key":"7_CR8","doi-asserted-by":"publisher","first-page":"743","DOI":"10.1007\/BF01213601","volume":"6","author":"K.R. Apt","year":"1994","unstructured":"Apt, K.R., Marchiori, E.: Reasoning about Prolog programs: from modes through types to assertions. Formal Aspects of Computing\u00a06(6A), 743\u2013765 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"7_CR9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines","author":"E. B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E.: Abstract State Machines. Springer, Heidelberg (2003)"},{"key":"7_CR10","unstructured":"Bowen, J.P.: Formal Specification and Documentation using Z. International Thomson Computer Press (1996)"},{"key":"7_CR11","unstructured":"Buckley, A.: Jsr-000202 JavaTM class file specification update evaluation 1.0 final release. Technical report (December 2006), http:\/\/jcp.org\/en\/jsr\/detail?id=202"},{"key":"7_CR12","unstructured":"ClearSy, Aix-en-Provence, France. B4Free: Tool and Manuals (2006), http:\/\/www.b4free.com"},{"key":"7_CR13","first-page":"238","volume-title":"Proceedings of the 4th ACM Symposium on Principles of Programming Languages, Los Angeles","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, Los Angeles, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"7_CR14","unstructured":"Dold, A., Gaul, T., Vialard, V., Zimmermann, W.: Asm-based mechanized verification of compiler back-ends. In: Workshop on Abstract State Machines, pp. 50\u201367 (1998)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/3-540-46562-6_42","volume-title":"Perspectives of System Informatics","author":"A. Dold","year":"2000","unstructured":"Dold, A., Vialard, V.: Formal verification of a compiler back-end generic checker program. In: Bj\u00f8rner, D., Broy, M., Zamulin, A.V. (eds.) PSI 1999. LNCS, vol.\u00a01755, pp. 470\u2013480. Springer, Heidelberg (2000)"},{"issue":"4","key":"7_CR16","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1142\/S0129054103001947","volume":"14","author":"A. Dold","year":"2003","unstructured":"Dold, A., von Henke, F.W., Goerigk, W.: A completely verified realistic bootstrap compiler. Int. J. Found. Comput. Sci.\u00a014(4), 659 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-540-69611-7_7","volume-title":"Practical Aspects of Declarative Languages","author":"M. Eichberg","year":"2006","unstructured":"Eichberg, M., Kahl, M., Saha, D., Mezini, M., Ostermann, K.: Automatic incrementalization of prolog based static analyses. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 109\u2013123. Springer, Heidelberg (2006)"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/11955757_24","volume-title":"B 2007: Formal Specification and Development in B","author":"N. Evans","year":"2006","unstructured":"Evans, N., Ifill, W.: Hardware verification and beyond: Using B at AWE. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol.\u00a04355, pp. 260\u2013261. Springer, Heidelberg (2006)"},{"issue":"1","key":"7_CR19","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/j.entcs.2007.02.062","volume":"190","author":"M. G\u00f3mez-Zamalloa","year":"2007","unstructured":"G\u00f3mez-Zamalloa, M., Albert, E., Puebla, G.: Improving the decompilation of java bytecode to prolog by partial evaluation. Electr. Notes Theor. Comput. Sci.\u00a0190(1), 85\u2013101 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"4","key":"7_CR20","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Prog. Lang. Syst.\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-540-69611-7_21","volume-title":"Practical Aspects of Declarative Languages","author":"K. Klose","year":"2006","unstructured":"Klose, K., Ostermann, K., Leuschel, M.: Partial evaluation of pointcuts. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 320\u2013334. Springer, Heidelberg (2006)"},{"issue":"1-2","key":"7_CR22","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1023\/A:1023072104553","volume":"16","author":"E.I. Leonard","year":"2003","unstructured":"Leonard, E.I., Heitmeyer, C.L.: Program synthesis from formal requirements specifications using apts. Higher-Order and Symbolic Computation\u00a016(1-2), 63\u201392 (2003)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"7_CR23","first-page":"42","volume-title":"33rd symposium Principles of Programming Languages","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd symposium Principles of Programming Languages, pp. 42\u201354. ACM Press, New York (2006)"},{"issue":"1","key":"7_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X. Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning\u00a041(1), 1\u201331 (2008)","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Leuschel, M.: Towards demonstrably correct compilation of java byte code. Technical report, Institut f\u00fcr Informaitk, Universit\u00e4t D\u00fcsseldorf (2009), http:\/\/www.stups.uni-duesseldorf.de\/~leuschel\/publication.php","DOI":"10.1007\/978-3-642-04167-9_7"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"McCarthy, J., Painter, J.: Correctness of a compiler for arithmetic expressions. Technical report, MIT AI Lab Memo (1967)","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"7_CR27","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/1315580.1315602","volume-title":"SIGAda","author":"C. Nettleton","year":"2007","unstructured":"Nettleton, C., Ifill, W., Marsh, C.: Towards a demonstrably-correct Ada compiler. In: Srivastava, A., Baird III, L.C. (eds.) SIGAda, pp. 89\u201396. ACM, New York (2007)"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/3-540-58431-5_3","volume-title":"Algebraic and Logic Programming","author":"R. Paige","year":"1994","unstructured":"Paige, R.: Viewing a program transformation system at work. In: Rodr\u00edguez-Artalejo, M., Levi, G. (eds.) ALP 1994. LNCS, vol.\u00a0850, p. 5. Springer, Heidelberg (1994)"},{"key":"7_CR29","unstructured":"Pichardie, D.: Bicolano \u2013 Byte Code Language in Coq. Summary appears in Mobius Deliverable 3.1 (2006), http:\/\/mobius.inria.fr\/bicolano"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-540-73210-5_25","volume-title":"Integrated Formal Methods","author":"D. Plagge","year":"2007","unstructured":"Plagge, D., Leuschel, M.: Validating Z Specifications using the ProB Animator and Model Checker. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 480\u2013500. Springer, Heidelberg (2007)"},{"issue":"4","key":"7_CR31","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s10817-007-9096-8","volume":"40","author":"L. Rideau","year":"2008","unstructured":"Rideau, L., Serpette, B.P., Leroy, X.: Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves. Journal of Automated Reasoning\u00a040(4), 307\u2013326 (2008)","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR32","unstructured":"Schmidt, D.: Denotational Semantics: a Methodology for Language Development. W.C. Brown Publishers (1986)"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/10720327_6","volume-title":"Logic-Based Program Synthesis and Transformation","author":"J.-G. Smaus","year":"2000","unstructured":"Smaus, J.-G., Hill, P.M., King, A.: Mode analysis domains for typed logic programs. In: Bossi, A. (ed.) LOPSTR 1999. LNCS, vol.\u00a01817, pp. 82\u2013101. Springer, Heidelberg (2000)"},{"key":"7_CR34","volume-title":"Virtual Machines: Versatile Platforms for Systems and Processes","author":"J. Smith","year":"2005","unstructured":"Smith, J., Nair, R.: Virtual Machines: Versatile Platforms for Systems and Processes. Morgan Kaufmann, San Francisco (2005)"},{"key":"7_CR35","unstructured":"Sorensen, I.: A mathematical AMN state based description of the ASP. Technical report, AWE (1998)"},{"key":"7_CR36","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall International Series in Computer Science (1992)"},{"key":"7_CR37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59495-3","volume-title":"Java and the Java Virtual Machine","author":"R.F. St\u00e4rk","year":"2001","unstructured":"St\u00e4rk, R.F., Schmid, J., B\u00f6rger, E.: Java and the Java Virtual Machine. Springer, Heidelberg (2001)"},{"key":"7_CR38","unstructured":"Stepney, S., Nabney, I.T.: The DeCCo project papers I-VI. Technical Report YCS-2002-358 \u2013 YCS-2002-363, Department of Computer Science, University of York (June 2003)"},{"key":"7_CR39","first-page":"17","volume-title":"35th symposium Principles of Programming Languages","author":"J.-B. Tristan","year":"2008","unstructured":"Tristan, J.-B., Leroy, X.: Formal verification of translation validators: A case study on instruction scheduling optimizations. In: 35th symposium Principles of Programming Languages, pp. 17\u201327. ACM Press, New York (2008)"},{"key":"7_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-540-30557-6_9","volume-title":"Practical Aspects of Declarative Languages","author":"Q. Wang","year":"2005","unstructured":"Wang, Q., Gupta, G., Leuschel, M.: Towards provably correct code generation via horn logical continuation semantics. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2004. LNCS, vol.\u00a03350, pp. 98\u2013112. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04167-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T22:30:24Z","timestamp":1558477824000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04167-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642041662","9783642041679"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04167-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}