{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:36:26Z","timestamp":1725539786456},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642045691"},{"type":"electronic","value":"9783642045707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04570-7_14","type":"book-chapter","created":{"date-parts":[[2009,11,2]],"date-time":"2009-11-02T23:51:23Z","timestamp":1257205883000},"page":"181-196","source":"Crossref","is-referenced-by-count":2,"title":["A Certified Implementation on Top of the Java Virtual Machine"],"prefix":"10.1007","author":[{"given":"Javier","family":"de Dios","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ricardo","family":"Pe\u00f1a","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Berghofer, S., Strecker, M.: Extracting a formally verified, fully executable compiler from a proof assistant. In: Proc. Compiler Optimization Meets Compiler Verification, COCV 2003. ENTCS, pp. 33\u201350 (2003)"},{"key":"14_CR2","series-title":"EATCS","volume-title":"Texts in Theoretical Computer Science","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Casteran, P.: Interactive Theorem Proving and Program Development Coq\u2019Art: The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science. EATCS. Springer, Heidelberg (2004)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/11813040_31","volume-title":"FM 2006: Formal Methods","author":"S. Blazy","year":"2006","unstructured":"Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 460\u2013475. Springer, Heidelberg (2006)"},{"issue":"6","key":"14_CR4","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/966221.966235","volume":"28","author":"M.A. Dave","year":"2003","unstructured":"Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Software Engineering Notes\u00a028(6), 2 (2003)","journal-title":"SIGSOFT Software Engineering Notes"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/978-3-642-03359-9_15","volume-title":"TPHOL 2009","author":"J. Dios de","year":"2009","unstructured":"de Dios, J., Pe\u00f1a, R.: Formal Certification of a Resource-Aware Language Implementation. In: Berghofer, S., et al. (eds.) TPHOL 2009. LNCS, vol.\u00a05674, pp. 196\u2013212. Springer, Heidelberg (2009)"},{"key":"14_CR6","unstructured":"Klein, G.: Verified Java Bytecode Verification, PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2003)"},{"key":"14_CR7","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/S0304-3975(02)00869-1","volume":"298","author":"G. Klein","year":"2003","unstructured":"Klein, G., Nipkow, T.: Verified Bytecode Verifiers. Theoretical Computer Science\u00a0298, 583\u2013626 (2003)","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"14_CR8","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 Transactions on Programming Languages and Systems\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"14_CR9","unstructured":"Klein, G., Nipkow, T., Schirmer, N., Strecker, M., Wildmoser, M.: Project VerifiCard (2001\u20132003), \n                    \n                      http:\/\/isabelle.in.tum.de\/VerifiCard\/"},{"key":"14_CR10","first-page":"42","volume-title":"Principles of Programming Languages, POPL 2006","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Principles of Programming Languages, POPL 2006, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"14_CR11","unstructured":"Leroy, X.: A formally verified compiler back-end, 79 pages (July 2008) (submitted)"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-540-71316-6_15","volume-title":"Programming Languages and Systems","author":"G. Li","year":"2007","unstructured":"Li, G., Owens, S., Slind, K.: Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 205\u2013219. Springer, Heidelberg (2007)"},{"key":"14_CR13","series-title":"The Java Series","volume-title":"The Java Virtual Machine Sepecification","author":"T. Lindholm","year":"1999","unstructured":"Lindholm, T., Yellin, F.: The Java Virtual Machine Sepecification, 2nd edn. The Java Series. Addison-Wesley, Reading (1999)","edition":"2"},{"key":"14_CR14","unstructured":"Montenegro, M., Pe\u00f1a, R., Segura, C.: A Simple Region Inference Algorithm for a First-Order Functional Language. In: Trends in Functional Programming, TFP 2008, Nijmegen (The Netherlands), May 2008, pp. 194\u2013208 (2008)"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Montenegro, M., Pe\u00f1a, R., Segura, C.: A Type System for Safe Memory Management and its Proof of Correctness. In: ACM Principles and Practice of Declarative Programming, PPDP 2008, Valencia, Spain, July 2008, pp. 152\u2013162 (2008)","DOI":"10.1145\/1389449.1389468"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-00515-2_10","volume-title":"Selected papers of Logic-Based Program Sinthesis and Transformation, LOPSTR 2008","author":"M. Montenegro","year":"2009","unstructured":"Montenegro, M., Pe\u00f1a, R., Segura, C.: An Inference Algorithm for Guaranteeing Safe Destruction. In: Selected papers of Logic-Based Program Sinthesis and Transformation, LOPSTR 2008. LNCS, vol.\u00a05438, pp. 135\u2013151. Springer, Heidelberg (2009)"},{"key":"14_CR17","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"ACM SIGPLAN-SIGACT Principles of Programming Languages, POPL 1997","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-Carrying Code. In: ACM SIGPLAN-SIGACT Principles of Programming Languages, POPL 1997, pp. 106\u2013119. ACM Press, New York (1997)"},{"issue":"5","key":"14_CR18","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/358438.349314","volume":"35","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. SIGPLAN Notices\u00a035(5), 83\u201394 (2000)","journal-title":"SIGPLAN Notices"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","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":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"14_CR20","first-page":"109","volume-title":"Selected Papers of the 7th Symp. on Trends in Functional Programming, TFP 2006","author":"R. Pe\u00f1a","year":"2007","unstructured":"Pe\u00f1a, R., Segura, C., Montenegro, M.: A Sharing Analysis for SAFE. In: Selected Papers of the 7th Symp. on Trends in Functional Programming, TFP 2006, pp. 109\u2013128. Intellect, Bristol (2007)"},{"key":"14_CR21","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":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation Validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-49059-0_7","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"C. Pusch","year":"1999","unstructured":"Pusch, C.: Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle\/HOL. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 89\u2013103. Springer, Heidelberg (1999)"},{"key":"14_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/3-540-45620-1_5","volume-title":"Automated Deduction - CADE-18","author":"M. Strecker","year":"2002","unstructured":"Strecker, M.: Formal Verification of a Java Compiler in Isabelle. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 63\u201377. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04570-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,10]],"date-time":"2019-03-10T06:19:18Z","timestamp":1552198758000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04570-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642045691","9783642045707"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04570-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}