{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:40:19Z","timestamp":1725518419464},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_7","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"83-99","source":"Crossref","is-referenced-by-count":6,"title":["Preservation of Proof Obligations from Java to the Java Virtual Machine"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[]},{"given":"Mariela","family":"Pavlova","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G.: WYSISWYX: What you see is not what you execute. PhD thesis, Department of Computer Science, University of Wisconsin (2007)","DOI":"10.1007\/978-3-540-69149-5_22"},{"key":"7_CR2","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"255","volume-title":"Bytecode Semantics, Verification, Analysis and Transformation","author":"F.Y. Bannwart","year":"2005","unstructured":"Bannwart, F.Y., M\u00fcller, P.: A program logic for bytecode. In: Spoto, F. (ed.) Bytecode Semantics, Verification, Analysis and Transformation. Electronic Notes in Theoretical Computer Science, vol.\u00a0141, pp. 255\u2013273. Elsevier, Amsterdam (2005)"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11823230_20","volume-title":"Static Analysis","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Gr\u00e9goire, B., Kunz, C., Rezk, T.: Certificate translation for optimizing compilers. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 301\u2013317. Springer, Heidelberg (2006)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1007\/978-3-540-78739-6_28","volume-title":"European Symposium on Programming","author":"G. Barthe","year":"2008","unstructured":"Barthe, G., Kunz, C.: Certificate translation in abstract interpretation. In: Drossopoulou, S. (ed.) European Symposium on Programming, Budapest, Hungary. LNCS, vol.\u00a04960, pp. 368\u2013382. Springer, Heidelberg (2008)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/11679219_9","volume-title":"Formal Aspects in Security and Trust","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Rezk, T., Saabas, A.: Proof obligations preserving compilation. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol.\u00a03866, pp. 112\u2013126. Springer, Heidelberg (2006)"},{"key":"7_CR6","first-page":"1835","volume-title":"Symposium on Applied Computing","author":"L. Burdy","year":"2006","unstructured":"Burdy, L., Pavlova, M.: Java bytecode specification and verification. In: Symposium on Applied Computing, pp. 1835\u20131839. ACM Press, New York (2006)"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-540-78663-4_4","volume-title":"Trustworthy Global Computing","author":"B. Gr\u00e9goire","year":"2007","unstructured":"Gr\u00e9goire, B., Sacchini, J.: Combining a verification condition generator for a bytecode language with static analyses. In: Barthe, G., Fournet, C. (eds.) Trustworthy Global Computing. LNCS, vol.\u00a04912, pp. 23\u201340. Springer, Heidelberg (2007)"},{"key":"7_CR9","first-page":"42","volume-title":"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: Morrisett, J.G., Peyton Jones, S.L. (eds.) Principles of Programming Languages, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/978-3-540-78791-4_14","volume-title":"CC","author":"F. Logozzo","year":"2008","unstructured":"Logozzo, F., F\u00e4hndrich, M.: On the relative completeness of bytecode analysis versus source code analysis. In: Hendren, L. (ed.) CC. LNCS, vol.\u00a04959, pp. 197\u2013212. Springer, Heidelberg (2008)"},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/1292316.1292321","volume-title":"SAVCBS 2007: Proceedings of the 2007 conference on Specification and verification of component-based systems","author":"P. M\u00fcller","year":"2007","unstructured":"M\u00fcller, P., Nordio, M.: Proof-transforming compilation of programs with abrupt termination. In: SAVCBS 2007: Proceedings of the 2007 conference on Specification and verification of component-based systems, pp. 39\u201346. ACM Press, New York (2007)"},{"key":"7_CR12","first-page":"106","volume-title":"Principles of Programming Languages","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: Principles of Programming Languages, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"7_CR13","first-page":"333","volume-title":"Programming Languages Design and Implementation","author":"G.C. Necula","year":"1998","unstructured":"Necula, G.C., Lee, P.: The design and implementation of a certifying compiler. In: Programming Languages Design and Implementation, vol.\u00a033, pp. 333\u2013344. ACM Press, New York (1998)"},{"key":"7_CR14","volume-title":"Isabelle\/HOL. A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Nordio, M., M\u00fcller, P., Meyer, B.: Formalizing proof-transforming compilation of eiffel programs. Technical Report 587, ETH Zurich (2008)","DOI":"10.1007\/978-3-540-69824-1_18"},{"key":"7_CR16","unstructured":"Pavlova, M.: Specification and verification of Java bytecode. PhD thesis, Universit\u00e9 de Nice Sophia-Antipolis (2007)"},{"key":"7_CR17","first-page":"1","volume-title":"Principles of Programming Languages","author":"X. Rival","year":"2004","unstructured":"Rival, X.: Symbolic Transfer Functions-based Approaches to Certified Compilation. In: Principles of Programming Languages, pp. 1\u201313. ACM Press, New York (2004)"},{"issue":"3","key":"7_CR18","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/j.tcs.2006.12.020","volume":"373","author":"A. Saabas","year":"2007","unstructured":"Saabas, A., Uustalu, T.: A compositional natural semantics and Hoare logic for low-level languages. Theoretical Computer Science\u00a0373(3), 273\u2013302 (2007)","journal-title":"Theoretical Computer Science"},{"key":"7_CR19","first-page":"91","volume-title":"ACM Workshop on Partial Evaluation and Semantics-based Program Manipulation","author":"A. Saabas","year":"2008","unstructured":"Saabas, A., Uustalu, T.: Proof optimization for partial redundancy elimination. In: ACM Workshop on Partial Evaluation and Semantics-based Program Manipulation, pp. 91\u2013101. ACM Press, New York (2008)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:15:16Z","timestamp":1605762916000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}