{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:03:58Z","timestamp":1725516238656},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540705918"},{"type":"electronic","value":"9783540705925"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70592-5_27","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"642-666","source":"Crossref","is-referenced-by-count":0,"title":["Computing Stack Maps with Interfaces"],"prefix":"10.1007","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Besson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tiphaine","family":"Turpin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/3-540-47813-2_3","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G. Barthe","year":"2002","unstructured":"Barthe, G., Dufay, G., Jakubiec, L., Melo de Sousa, S.: A formal correspondence between offensive and defensive javacard virtual machines. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol.\u00a02294, pp. 32\u201345. Springer, Heidelberg (2002)"},{"key":"27_CR2","unstructured":"Besson, F., Jensen, T., Turpin, T.: Computing stack maps with interfaces. Technical Report 1879, Irisa (2007)"},{"key":"27_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-71316-6_19","volume-title":"Programming Languages and Systems","author":"F. Besson","year":"2007","unstructured":"Besson, F., Jensen, T., Turpin, T.: Small witnesses for abstract interpretation-based proofs. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 268\u2013283. Springer, Heidelberg (2007)"},{"key":"27_CR4","unstructured":"Bracha, G., Lindholm, T., Tao, W., Yellin, F.: CLDC Byte Code Typechecker Specification. Sun Microsystems (2003)"},{"key":"27_CR5","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1145\/512950.512973","volume-title":"Proc. of the 4th ACM Symp.\u00a0on Principles of Programming Languages (POPL 1977)","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixpoints. In: Proc. of the 4th ACM Symp.\u00a0on Principles of Programming Languages (POPL 1977), pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"27_CR6","volume-title":"Introduction to Lattices and Order","author":"B.A. Davey","year":"1990","unstructured":"Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press, Cambridge (1990)","edition":"2"},{"issue":"3-4","key":"27_CR7","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1023\/A:1025011624925","volume":"30","author":"S.N. Freund","year":"2003","unstructured":"Freund, S.N., Mitchell, J.C.: A type system for the java bytecode language and verifier. Journal of Automated Reasoning\u00a030(3-4), 271\u2013321 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"27_CR8","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/288090.288104","volume-title":"Proc. of the 5th ACM conference on Computer and Communications Security (CCS 1998)","author":"A. Goldberg","year":"1998","unstructured":"Goldberg, A.: A specification of java loading and bytecode verification. In: Proc. of the 5th ACM conference on Computer and Communications Security (CCS 1998), pp. 49\u201358. ACM Press, New York (1998)"},{"key":"27_CR9","unstructured":"JSR 202 Expert Group. Java Class File Specification Update, Sun Microsystems (2006)"},{"issue":"2","key":"27_CR10","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1145\/383043.383045","volume":"23","author":"T.B. Knoblock","year":"2001","unstructured":"Knoblock, T.B., Rehof, J.: Type elaboration and subtype completion for java bytecode. ACM Transactions on Programming Languages and Systems\u00a023(2), 243\u2013272 (2001)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3-4","key":"27_CR11","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1023\/A:1025055424017","volume":"30","author":"X. Leroy","year":"2003","unstructured":"Leroy, X.: Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning\u00a030(3-4), 235\u2013269 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"27_CR12","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1145\/268946.268979","volume-title":"Proc. of the 25th ACM Symp. on Principles of Programming Languages (POPL 1998)","author":"X. Leroy","year":"1998","unstructured":"Leroy, X., Rouaix, F.: Security properties of typed applets. In: Proc. of the 25th ACM Symp. on Principles of Programming Languages (POPL 1998), pp. 391\u2013403. ACM Press, New York (1998)"},{"key":"27_CR13","volume-title":"The Java Virtual Machine Specification","author":"T. Lindholm","year":"1999","unstructured":"Lindholm, T., Yellin, F.: The Java Virtual Machine Specification, 2nd edn. Prentice-Hall, Englewood Cliffs (1999)","edition":"2"},{"key":"27_CR14","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":"27_CR15","doi-asserted-by":"crossref","unstructured":"Qian, Z.: A formal specification of java virtual machine instructions for objects, methods and subrountines. In: Formal Syntax and Semantics of Java, pp. 271\u2013312 (1999)","DOI":"10.1007\/3-540-48737-9_8"},{"issue":"3-4","key":"27_CR16","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. Journal of Automated Reasoning\u00a031(3-4), 303\u2013334 (2003)","journal-title":"Journal of Automated Reasoning"},{"issue":"6","key":"27_CR17","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/1286821.1286830","volume":"29","author":"S. Seo","year":"2007","unstructured":"Seo, S., Yang, H., Yi, K., Han, T.: Goal-directed weakening of abstract interpretation results. ACM Transactions on Programming Languages and Systems\u00a029(6), 39 (2007)","journal-title":"ACM Transactions on Programming Languages and Systems"}],"container-title":["Lecture Notes in Computer Science","ECOOP 2008 \u2013 Object-Oriented Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70592-5_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:08:27Z","timestamp":1605762507000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70592-5_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705918","9783540705925"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70592-5_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}