M. Abadi, A. Banerjee, N. Heintze, and J. G. Riecke, A core calculus of dependency, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.147-160, 1999.
DOI : 10.1145/292540.292555

D. Basin, S. Friedrich, and M. Gawkowski, Java Bytecode Verification by Model Checking, Journal of Automated Reasoning. Special issue on bytecode verification
DOI : 10.1007/3-540-48683-6_43

Y. Bertot, Formalizing a JVML Verifier for Initialization in a Theorem Prover, Proc. Computer Aided Verification (CAV'01), pp.14-24, 2001.
DOI : 10.1007/3-540-44585-4_3

P. Brisset, Vers un vérifieur de bytecode Java certifié. Seminar given at Ecole Normale Supérieure, 1998.

K. Brunnstein, Hostile ActiveX control demonstrated, RISKS Forum, vol.18, issue.82, 1997.

Z. Chen, Java Card Technology for Smart Cards: Architecture and Programmer's Guide. The Java Series, 2000.

G. Chugunov, L. Fredlund, and D. Gurov, Model checking multi-applet Java Card applications, Smart Card Research and Advanced Applications Conference (CARDIS'02), 2002.

A. Coglio, Simple verification technique for complex Java bytecode subroutines, 4th ECOOP Workshop on Formal Techniques for Java-like Programs, 2002.
DOI : 10.1002/cpe.798
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.124.6884

A. Coglio, Improving the official specification of Java bytecode verification. Concurrency and Computation: Practice and Experience, pp.155-179, 2003.

A. Coglio, A. Goldberg, and Z. Qian, Toward a provably-correct implementation of the JVM bytecode verifier, Proceedings DARPA Information Survivability Conference and Exposition. DISCEX'00, 1998.
DOI : 10.1109/DISCEX.2000.821537

R. Cohen, The defensive Java virtual machine specification, Computational Logic Inc, 1997.

D. Deville and G. Grimaud, Building an " impossible " verifier on a Java Card, USENIX Workshop on Industrial Experiences with Systems Software (WIESS'02), 2002.

N. Stephen, J. C. Freund, and . Mitchell, A type system for the Java bytecode language and verifier, Journal of Automated Reasoning. Special issue on bytecode verification

N. Stephen, J. C. Freund, and . Mitchell, A formal framework for the java bytecode language and verifier, Object-Oriented Programming Systems, Languages and Applications 1999, pp.147-166, 1999.

N. Stephen, J. C. Freund, and . Mitchell, A type system for object initialization in the Java bytecode language, ACM Transactions on Programming Languages and Systems, vol.21, issue.6, pp.1196-1250, 1999.

A. Frey, On-terminal verifier for JEFF files, 2001.

A. Goldberg, A specification of Java loading and bytecode verification, Proceedings of the 5th ACM conference on Computer and communications security , CCS '98, pp.49-58, 1998.
DOI : 10.1145/288090.288104

L. Gong, Inside Java 2 platform security: architecture, API design, and implementation. The Java Series, 1999.

J. A. Gosling, Java intermediate bytecodes, Proc. ACM SIGPLAN Workshop on Intermediate Representations, pp.111-118, 1995.
DOI : 10.1145/202530.202541

M. Hagiya and A. Tozawa, On a New Method for Dataflow Analysis of Java Virtual Machine Subroutines, SAS'98, pp.17-32, 1998.
DOI : 10.1007/3-540-49727-7_2

H. Pieter, . Hartel, A. V. Luc, and . Moreau, Formalizing the safety of Java, the Java virtual machine and Java Card, ACM Computing Surveys, vol.33, issue.4, pp.517-558, 2001.

N. Heintze and J. G. Riecke, The SLam calculus, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.365-377, 1998.
DOI : 10.1145/268946.268976

L. Henrio and B. Serpette, A framework for bytecode verifiers: Application to intra-procedural continuations, Research report, 2001.

M. Huisman, B. Jacobs, J. Van-den, and . Berg, A case study in class library verification: Java's Vector class. Software Tools for Technology Transfer, pp.332-352, 2001.

T. Jensen, D. L. Métayer, and T. Thorn, Verification of control flow based security properties, Proceedings of the 1999 IEEE Symposium on Security and Privacy (Cat. No.99CB36344), 1999.
DOI : 10.1109/SECPRI.1999.766902

G. Klein and M. Wildmoser, Verified Bytecode Subroutines, Journal of Automated Reasoning. Special issue on bytecode verification
DOI : 10.1007/10930755_4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.9059

G. Klein, Verified Java bytecode verification, 2003.

G. Klein and T. Nipkow, Verified lightweight bytecode verification. Concurrency and Computation: Practice and Experience, pp.1133-1151, 2001.
DOI : 10.1002/cpe.597
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.152.7227

G. Klein and T. Nipkow, Verified bytecode verifiers, Theoretical Computer Science, vol.298, issue.3, 2002.
DOI : 10.1016/S0304-3975(02)00869-1
URL : http://doi.org/10.1016/s0304-3975(02)00869-1

T. Knoblock and J. Rehof, Type elaboration and subtype completion for Java bytecode, 27th symposium Principles of Programming Languages, pp.228-242, 2000.
DOI : 10.1145/383043.383045
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.6118

X. Leroy, Bytecode verification on Java smart cards, Software: Practice and Experience, vol.21, issue.4, pp.319-340, 2002.
DOI : 10.1002/spe.438
URL : https://hal.archives-ouvertes.fr/hal-01499944

X. Leroy and F. Rouaix, Security Properties of Typed Applets, Secure Internet Programming ? Security issues for Mobile and Distributed Objects, pp.147-182, 1999.
DOI : 10.1007/3-540-48749-2_7
URL : https://hal.archives-ouvertes.fr/hal-01499957

T. Lindholm and F. Yellin, The Java Virtual Machine Specification. The Java Series, 1999.

S. Steven and . Muchnick, Advanced compiler design and implementation, 1997.

C. George and . Necula, Proof-carrying code, 24th symposium Principles of Programming Languages, pp.106-119, 1997.

F. Nielson, H. R. Nielson, and C. Hankin, Principles of program analysis, 1999.
DOI : 10.1007/978-3-662-03811-6

T. Nipkow, Verified Bytecode Verifiers, Foundations of Software Science and Computation Structures, pp.347-363, 2001.
DOI : 10.1007/3-540-45315-6_23

O. Robert and . Callahan, A simple, comprehensive type system for Java bytecode subroutines, 26th symposium Principles of Programming Languages, pp.70-78, 1999.

J. Posegga and H. Vogt, Java bytecode verification using model checking, Workshop Fundamental Underpinnings of Java, 1998.

F. Pottier and V. Simonet, Information flow inference for ML, 29th symposium Principles of Programming Languages, pp.319-330, 2002.
DOI : 10.1145/565816.503302
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.157.6266

F. Pottier, C. Skalka, and S. Smith, A systematic approach to static access control, Proceedings of the 10th European Symposium on Programming, pp.30-45, 2001.
DOI : 10.1145/1057387.1057392
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.2800

C. Pusch, Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL, TACAS'99, pp.89-103, 1999.
DOI : 10.1007/3-540-49059-0_7

Z. Qian, A formal specification of Java virtual machine instructions for objects, methods and subroutines, Formal syntax and semantics of Java, 1998.

Z. Qian, Standard fixpoint iteration for Java bytecode verification, ACM Transactions on Programming Languages and Systems, vol.22, issue.4, pp.638-672, 2000.
DOI : 10.1145/363911.363915
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.1730

E. Rose, Vérification de code d'octet de la machine virtuelle Java: formalisation et implantation, 2002.

E. Rose and K. Rose, Lightweight Bytecode Verification, OOPSLA Workshop on Formal Underpinnings of Java, 1998.
DOI : 10.1023/B:JARS.0000021015.15794.82
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.647

A. David and . Schmidt, Data flow analysis is model checking of abstract interpretations, 25th symposium Principles of Programming Languages, pp.38-48, 1998.

R. Stärk, J. Schmid, and E. Börger, Java and the Java Virtual Machine, 2001.
DOI : 10.1007/978-3-642-59495-3

F. Robert, J. Stärk, and . Schmid, Completeness of a bytecode verifier and a certifying Java-to-JVM compiler, Journal of Automated Reasoning. Special issue on bytecode verification

R. Stata and M. Abadi, A type system for Java bytecode subroutines, ACM Transactions on Programming Languages and Systems, vol.21, issue.1, pp.90-137, 1999.
DOI : 10.1145/314602.314606
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.152.2904

S. Microsystems, Java 2 platform micro edition technology for creating mobile devices. White paper, 2000.

T. Logic, Off-card bytecode verifier for Java Card. Distributed as part of Sun's Java Card Development Kit, 2001.

G. Vigna, Mobile Agents and Security, volume 1419 of Lecture Notes in Computer Science, 1998.

D. Volpano and G. Smith, A type-based approach to program security, Proceedings of TAPSOFT'97, Colloquium on Formal Approaches in Software Engineering, pp.607-621, 1997.
DOI : 10.1007/BFb0030629
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.152.7398

D. Volpano, G. Smith, and C. Irvine, A sound type system for secure flow analysis, Journal of Computer Security, vol.4, issue.2-3, pp.1-21, 1996.
DOI : 10.3233/JCS-1996-42-304
URL : http://doi.org/10.3233/jcs-1996-42-304

D. Walker, A type system for expressive security policies, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '00, pp.254-267, 2000.
DOI : 10.1145/325694.325728
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1.4759

F. Yellin, Low level security in Java, Proceedings of the Fourth International World Wide Web Conference, pp.369-379, 1995.