{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T12:48:37Z","timestamp":1749818917985,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642171635"},{"type":"electronic","value":"9783642171642"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-17164-2_8","type":"book-chapter","created":{"date-parts":[[2010,11,19]],"date-time":"2010-11-19T05:54:39Z","timestamp":1290146079000},"page":"97-113","source":"Crossref","is-referenced-by-count":12,"title":["A Provably Correct Stackless Intermediate Representation for Java Bytecode"],"prefix":"10.1007","author":[{"given":"Delphine","family":"Demange","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","first-page":"127","volume-title":"Proc. of SEFM 2008","author":"G. Barthe","year":"2008","unstructured":"Barthe, G., Kunz, C., Pichardie, D., Samborski-Forlese, J.: Preservation of proof obligations for hybrid verification methods. In: Proc. of SEFM 2008, pp. 127\u2013136. IEEE Computer Society, Los Alamitos (2008)"},{"issue":"3","key":"8_CR2","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/j.tcs.2006.08.012","volume":"364","author":"F. Besson","year":"2006","unstructured":"Besson, F., Jensen, T., Pichardie, D.: Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci.\u00a0364(3), 273\u2013291 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR3","first-page":"129","volume-title":"Proc. of JAVA 1999","author":"M.G. Burke","year":"1999","unstructured":"Burke, M.G., Choi, J., Fink, S., Grove, D., Hind, M., Sarkar, V., Serrano, M.J., Sreedhar, V.C., Srinivasan, H., Whaley, J.: The Jalape\u00f1o dynamic optimizing compiler for Java. In: Proc. of JAVA 1999, pp. 129\u2013141. ACM, New York (1999)"},{"issue":"3","key":"8_CR4","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1109\/40.591653","volume":"17","author":"T. Cramer","year":"1997","unstructured":"Cramer, T., Friedman, R., Miller, T., Seberger, D., Wilson, R., Wolczko, M.: Compiling Java just in time. IEEE Micro\u00a017(3), 36\u201343 (1997)","journal-title":"IEEE Micro"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Demange, D., Jensen, T., Pichardie, D.: A provably correct stackless intermediate representation for Java bytecode. Research Report 7021, INRIA (2009), \n                    \n                      http:\/\/www.irisa.fr\/celtique\/ext\/bir\/rr7021.pdf","DOI":"10.1007\/978-3-642-17164-2_8"},{"issue":"6","key":"8_CR6","doi-asserted-by":"publisher","first-page":"1196","DOI":"10.1145\/330643.330646","volume":"21","author":"S.N. Freund","year":"1999","unstructured":"Freund, S.N., Mitchell, J.C.: The type system for object initialization in the Java bytecode language. ACM TOPLAS\u00a021(6), 1196\u20131250 (1999)","journal-title":"ACM TOPLAS"},{"issue":"4","key":"8_CR7","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 TOPLAS\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM TOPLAS"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-540-78791-4_14","volume-title":"Compiler Construction","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 2008. LNCS, vol.\u00a04959, pp. 197\u2013212. Springer, Heidelberg (2008)"},{"key":"8_CR9","first-page":"249","volume-title":"PPDP 2006: Proceedings of the 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming","author":"Y. Matsuno","year":"2006","unstructured":"Matsuno, Y., Ohori, A.: A type system equivalent to static single assignment. In: PPDP 2006: Proceedings of the 8th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 249\u2013260. ACM, New York (2006)"},{"key":"8_CR10","unstructured":"The Jikes\u00a0RVM Project. Jikes rvm - home page, \n                    \n                      http:\/\/jikesrvm.org"},{"issue":"3-4","key":"8_CR11","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1023\/B:JARS.0000021015.15794.82","volume":"31","author":"E. Rose","year":"2003","unstructured":"Rose, E.: Lightweight bytecode verification. J. Autom. Reason.\u00a031(3-4), 303\u2013334 (2003)","journal-title":"J. Autom. Reason."},{"key":"8_CR12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59495-3","volume-title":"Java and the Java Virtual Machine: Definition, Verification, Validation with Cdrom","author":"R.F. Stark","year":"2001","unstructured":"Stark, R.F., Borger, E., Schmid, J.: Java and the Java Virtual Machine: Definition, Verification, Validation with Cdrom. Springer, New York (2001)"},{"key":"8_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","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)"},{"key":"8_CR14","unstructured":"Vall\u00e9e-Rai, R., Co, P., Gagnon, E., Hendren, L., Lam, P., Sundaresan, V.: Soot - a Java bytecode optimization framework. In: Proc. of CASCON 1999. IBM Press (1999)"},{"key":"8_CR15","unstructured":"Vallee-Rai, R., Hendren, L.J.: Jimple: Simplifying Java bytecode for analyses and transformations (1998)"},{"key":"8_CR16","unstructured":"Whaley, J.: Dynamic optimization through the use of automatic runtime specialization. Master\u2019s thesis, Massachusetts Institute of Technology (May 1999)"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Wildmoser, M., Chaieb, A., Nipkow, T.: Bytecode analysis for proof carrying code. In: Proc. of BYTECODE 2005, Electronic Notes in Computer Science (2005)","DOI":"10.1016\/j.entcs.2005.02.040"},{"key":"8_CR18","unstructured":"Xi, H., Xia, S.: Towards array bound check elimination in Java tm virtual machine language. In: Proc. of CASCON 1999, p. 14. IBM Press (1999)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17164-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T19:16:35Z","timestamp":1558293395000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17164-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642171635","9783642171642"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17164-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}