{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T06:50:48Z","timestamp":1672296648336},"reference-count":20,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2003,3,1]],"date-time":"2003-03-01T00:00:00Z","timestamp":1046476800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3827,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2003,3]]},"DOI":"10.1016\/s0167-6423(02)00095-3","type":"journal-article","created":{"date-parts":[[2002,11,5]],"date-time":"2002-11-05T13:14:20Z","timestamp":1036502060000},"page":"283-306","source":"Crossref","is-referenced-by-count":4,"title":["A B model for ensuring soundness of a large subset of the Java Card virtual machine"],"prefix":"10.1016","volume":"46","author":[{"given":"Antoine","family":"Requet","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0167-6423(02)00095-3_BIB1","unstructured":"M. Abadi, R. Stata, A type system for byte code subroutines, in: Proc. 25th ACM Symp. on Principle of Programming Languages, January 1998."},{"key":"10.1016\/S0167-6423(02)00095-3_BIB2","series-title":"The B Book, Assigning Programs to Meanings","author":"Abrial","year":"1996"},{"key":"10.1016\/S0167-6423(02)00095-3_BIB3","unstructured":"M. Alberda, P. Hartel, E. de Jong, Using formal methods to cultivate trust in Smart Card operating system, in: Proc. Second Smart Card Research and Advanced Applications Conference (CARDIS\u201996), Amsterdam, Netherlands, September 1996, pp. 111\u2013132."},{"key":"10.1016\/S0167-6423(02)00095-3_BIB4","unstructured":"L. Casset, J.-L. Lanet, A formal specification of the Java byte code semantics using the B method, in: Proc. ECOOP\u201999 Workshop on Formal Techniques for Java Programs, June 1999."},{"key":"10.1016\/S0167-6423(02)00095-3_BIB5","unstructured":"Cohen, Defensive Java Virtual Machine Specification, URL: http:\/\/www.cli.com\/software\/djvm."},{"key":"10.1016\/S0167-6423(02)00095-3_BIB6","doi-asserted-by":"crossref","unstructured":"E. Denney, T. Jensen, Correctness of Java Card method lookup via logical relations, in: Smolka (Ed.), European Symp. on Programming (ESOP 2000), Lecture Notes in Computer Science, vol. 1782, Springer, Berlin, March 2000, pp. 104\u2013118. URL: http:\/\/www.irisa.fr\/lande\/jensen\/papers\/esop00.ps.","DOI":"10.1007\/3-540-46425-5_7"},{"key":"10.1016\/S0167-6423(02)00095-3_BIB7","doi-asserted-by":"crossref","unstructured":"S.N. Freund, J.C. Mitchell, A type system for object initialization in the Java byte code language, in: Proc. ACM Conf. on Object-Oriented Programming Systems, Languages and Applications, October 1998.","DOI":"10.1145\/286936.286972"},{"key":"10.1016\/S0167-6423(02)00095-3_BIB8","unstructured":"S.N. Freund, J.C. Mitchell, Specification and verification of Java bytecode subroutines and exceptions, Stanford Computer Science Technical Note, August 1999."},{"key":"10.1016\/S0167-6423(02)00095-3_BIB9","doi-asserted-by":"crossref","unstructured":"A. Goldberg, A Specification of Java Loading and Byte Code Verification, Kestrel Institute, December 1997. URL: http:\/\/www.kestrel.edu\/HTML\/people\/goldberg.","DOI":"10.1145\/288090.288104"},{"key":"10.1016\/S0167-6423(02)00095-3_BIB10","unstructured":"Y. Gurevitch, C. Wallace, Specification and verification of the windows card runtime environment using abstract state machines, Microsoft Research Technical Report. http:\/\/www.eecs.umich.edu\/gasm\/papers\/wincard.html."},{"key":"10.1016\/S0167-6423(02)00095-3_BIB11","unstructured":"J.L. Lanet, A. Requet, Formal proof of smart card applets correctness, in: Quisquater, Schneier (Eds.), Third Smart Card Research and Advanced Application Conference (CARDIS\u201998), Louvain-la-Neuve, Belgium, September 1998, Lecture Notes in Computer Science, vol. 1820, Springer, Berlin, pp. 85\u201397."},{"key":"10.1016\/S0167-6423(02)00095-3_BIB12","series-title":"The Java Virtual Machine Specification","author":"Lindholm","year":"1996"},{"key":"10.1016\/S0167-6423(02)00095-3_BIB13","unstructured":"S. Motr\u00e9, Formal Proof of the Applet Firewall, AFADL 2000, Grenoble, France, February 2000. URL: http:\/\/www-lsr.imag.fr\/afadl\/Programme\/Articles\/."},{"key":"10.1016\/S0167-6423(02)00095-3_BIB14","doi-asserted-by":"crossref","unstructured":"T. Nipkow, D. Oheimb, Javalight is type-safe-definitely, in: 25th Proc. ACM Symp. on Principle of Programming Languages, January 1998.","DOI":"10.1145\/268946.268960"},{"key":"10.1016\/S0167-6423(02)00095-3_BIB15","doi-asserted-by":"crossref","unstructured":"J. Posegga, H. Vogt, Byte code verification for Java Smart Cards based on model checking, in: Quisquater, Deswarte, Meadows, Gollmann (Eds.), Proc. 5th European Symp. on Research in Computer Security (ESORICS 98), Louvain-la-neuve, Belgium, September 1998, Lecture Notes in Computer Science, vol. 1485, Springer, Berlin, pp. 175\u2013190.","DOI":"10.1007\/BFb0055863"},{"key":"10.1016\/S0167-6423(02)00095-3_BIB16","doi-asserted-by":"crossref","unstructured":"C. Pusch, Proving the soundness of a Java bytecode verifier specification in Isabelle\/HOL, in: Cleaveland (Ed.), TACAS 1999, Amsterdam, The Netherlands, March 1999, Lecture Notes in Computer Science, vol. 1579, Springer, Berlin, pp. 89\u2013103, URL: http:\/\/www.in.tum.de\/~pusch\/.","DOI":"10.1007\/3-540-49059-0_7"},{"key":"10.1016\/S0167-6423(02)00095-3_BIB17","unstructured":"Z. Qian, Least types for memory locations in Java byte code, Kestrel Institute, Technical Report, 1998."},{"key":"10.1016\/S0167-6423(02)00095-3_BIB18","unstructured":"S. Stepney, D. Cooper, Formal methods for industrial products, in: Bowen, Dunne, Galloway, King (Eds.), ZB\u20192000, New York, England 2000, Lecture Notes in Computer Science, vol. 1878, Springer, Berlin, pp. 364\u2013393."},{"key":"10.1016\/S0167-6423(02)00095-3_BIB19","unstructured":"Sun Microsystems, Java Card 2.1 Virtual Machine Specification, March 1999."},{"key":"10.1016\/S0167-6423(02)00095-3_BIB20","unstructured":"D. Syme, Proving Java type soundness, Technical Report, University of Cambridge, Computer Laboratory, 1997."}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642302000953?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642302000953?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,5]],"date-time":"2020-03-05T14:32:53Z","timestamp":1583418773000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642302000953"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,3]]},"references-count":20,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,3]]}},"alternative-id":["S0167642302000953"],"URL":"https:\/\/doi.org\/10.1016\/s0167-6423(02)00095-3","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2003,3]]}}}