{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:56:37Z","timestamp":1725566197029},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540230175"},{"type":"electronic","value":"9783540301424"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30142-4_21","type":"book-chapter","created":{"date-parts":[[2010,9,18]],"date-time":"2010-09-18T20:14:09Z","timestamp":1284840849000},"page":"287-304","source":"Crossref","is-referenced-by-count":1,"title":["Formalizing Java Dynamic Loading in HOL"],"prefix":"10.1007","author":[{"given":"Tian-jun","family":"Zuo","sequence":"first","affiliation":[]},{"given":"Jun-gang","family":"Han","sequence":"additional","affiliation":[]},{"given":"Ping","family":"Chen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/3-540-45685-6_4","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Barthe","year":"2002","unstructured":"Barthe, G., Courtieu, P.: A formal correspondence between offensive and defensive javacard virtual machines. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, pp. 31\u201346. Springer, Heidelberg (2002)"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/3-540-45309-1_20","volume-title":"Programming Languages and Systems","author":"G. Barthe","year":"2001","unstructured":"Barthe, G., Dufay, G., Jakubiec, L., Sousa, S.M., Serpette, B.P.: A formal executable semantics of the javacard platform. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, pp. 302\u2013319. Springer, Heidelberg (2001)"},{"key":"21_CR3","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., Sousa, S.M., Serpette, B.P.: A formal correspondence between offensive and defensive javacard virtual machines. In A. Cortesi, editor, Proc. VMCAI\u201902. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol.\u00a02294, pp. 32\u201345. Springer, Heidelberg (2002)"},{"doi-asserted-by":"crossref","unstructured":"Dean, D.: The security of static typing with dynamic linking. In: Fourth ACM Conference on Computer and Communication Security (1997)","key":"21_CR4","DOI":"10.1145\/266420.266428"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-45332-6_3","volume-title":"Types in Compilation","author":"S. Drossopoulou","year":"2001","unstructured":"Drossopoulou, S.: Towards an abstract model of java dynamic linking and verification. In: Harper, R. (ed.) TIC 2000. LNCS, vol.\u00a02071, pp. 53\u201384. Springer, Heidelberg (2001)"},{"issue":"4","key":"21_CR6","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1145\/363516.363523","volume":"9","author":"P.W.L. Fong","year":"2000","unstructured":"Fong, P.W.L., Cameron, R.D.: Proof linking: Modular verification of mobile programs in the presence of lazy, dynamic linking. ACM Transactions on Software Engineering and Methodology\u00a09(4), 379\u2013409 (2000)","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"doi-asserted-by":"crossref","unstructured":"Jensen, T., Le Metayer, D., Thorn, T.: Security and dynamic loading in java: A formalisation. In: Proceedings of the 1998 IEEE International Conference on Computer Languages, Chicago, Illinois, May 1998, vol.\u00a02618, pp. 4\u201315 (1998)","key":"21_CR7","DOI":"10.1109\/ICCL.1998.674152"},{"doi-asserted-by":"crossref","unstructured":"Klein, G.: Verified Java bytecode verification. PhD thesis, Technische Universitat Munchen (2003)","key":"21_CR8","DOI":"10.1016\/S0304-3975(02)00869-1"},{"unstructured":"Klein, G., Strecker, M.: Verified bytecode verification and typecertifying compilation. Journal of Logic Programming (2002)","key":"21_CR9"},{"doi-asserted-by":"crossref","unstructured":"Klein, G., Wildmoser, M.: Verified bytecode subroutines. Journal of Automated Reasoning, Special Issue on Bytecode Verification (2003)","key":"21_CR10","DOI":"10.1007\/10930755_4"},{"doi-asserted-by":"crossref","unstructured":"Liu, H., Moore, J.S.: Executable jvm model for analytical reasoning: a study. In: Proceedings of the 2003 workshop on Interpreters, Virtual Machines and Emulators, San Diego, California, pp. 15\u201323 (2003)","key":"21_CR11","DOI":"10.1145\/858570.858572"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-45315-6_23","volume-title":"Foundations of Software Science and Computation Structures","author":"T. Nipkow","year":"2001","unstructured":"Nipkow, T.: Verified bytecode verifiers. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol.\u00a02030, pp. 347\u2013363. Springer, Heidelberg (2001)"},{"key":"21_CR13","first-page":"117","volume-title":"Foundations of Secure Computation","author":"T. Nipkow","year":"2000","unstructured":"Nipkow, T., von Oheimb, D., Pusch, C.: \u03bcjava: Embedding a programming language in a theorem prover. In: Bauer, F.L., Steinbruggen, R. (eds.) Foundations of Secure Computation, pp. 117\u2013144. IOS Press, Amsterdam (2000)"},{"key":"21_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":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/3-540-48737-9_8","volume-title":"Formal Syntax and Semantics of Java","author":"Z. Qian","year":"1999","unstructured":"Qian, Z.: A formal specification of java-TM virtual machine instructions for objects, methods and subroutines. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java. LNCS, vol.\u00a01523, pp. 271\u2013311. Springer, Heidelberg (1999)"},{"doi-asserted-by":"crossref","unstructured":"Qian, Z., Goldberg, A., Coglio, A.: A formal specification of javatm class loading. In: OOPSLA 2000 (November 2000)","key":"21_CR16","DOI":"10.1145\/353171.353193"},{"unstructured":"Saraswat, V.: Java is not type-safe. Technical report, AT&T Rresearch (1997)","key":"21_CR17"},{"key":"21_CR18","volume-title":"The JavaTM Virtual Machine Specification","author":"T. Lindholm","year":"1999","unstructured":"Lindholm, T., Yellin, F.: The JavaTM Virtual Machine Specification, 2nd edn. Addison-Wesley, Reading (1999)","edition":"2"},{"unstructured":"Tozawa, A., Hagiya, M.: New fomalizaion of the JVM (1999), http:\/\/nicosia.is.s.u.-tokyo.ac.jp\/members\/milespapers\/cl-99.ps","key":"21_CR19"},{"unstructured":"von Oheimb, D.: Analyzing Java in Isabelle\/HOL: Formalization, Type Safety and Hoare Logic. PhD thesis, Technische Universitat Munchen (2001)","key":"21_CR20"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30142-4_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,10]],"date-time":"2021-11-10T00:22:36Z","timestamp":1636503756000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30142-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230175","9783540301424"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30142-4_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}