G. Barthe, G. Dufay, L. Jakubiec, S. Melo, and . Sousa, A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines, Proc. of the 3rd Int. Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI'02), pp.32-45, 2002.
DOI : 10.1007/3-540-47813-2_3

F. Besson, T. Jensen, and T. Turpin, Computing Stack Maps with Interfaces, 2007.
DOI : 10.1007/978-3-540-70592-5_27
URL : https://hal.archives-ouvertes.fr/inria-00332526

F. Besson, T. Jensen, and T. Turpin, Small witnesses for abstract interpretationbased proofs, Proc. of the 16th European Symp. on Programming, pp.268-283, 2007.

G. Bracha, T. Lindholm, W. Tao, and F. Yellin, CLDC Byte Code Typechecker Specification, 2003.

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973
URL : https://hal.archives-ouvertes.fr/inria-00528590

B. A. Davey and H. A. Priestley, Introduction to Lattices and Order, 1990.
DOI : 10.1017/CBO9780511809088

S. N. Freund and J. C. Mitchell, A type system for the java bytecode language and verifier, Journal of Automated Reasoning, vol.30, pp.3-4271, 2003.

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

T. B. Knoblock and J. Rehof, Type elaboration and subtype completion for Java bytecode, ACM Transactions on Programming Languages and Systems, vol.23, issue.2, pp.243-272, 2001.
DOI : 10.1145/383043.383045

X. Leroy, Java bytecode verification: algorithms and formalizations, Journal of Automated Reasoning, vol.30, issue.3/4, pp.235-269, 2003.
DOI : 10.1023/A:1025055424017
URL : https://hal.archives-ouvertes.fr/hal-01499939

X. Leroy and F. Rouaix, Security properties of typed applets, Proc. of the 25th ACM Symp. on Principles of Programming Languages (POPL'98), pp.391-403, 1998.
URL : https://hal.archives-ouvertes.fr/hal-01499957

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

C. Pusch, Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL, Proc. of the 5th Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems (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 subrountines. Formal Syntax and Semantics of Java, pp.271-312, 1999.

E. Rose, Lightweight Bytecode Verification, Journal of Automated Reasoning, vol.31, issue.3/4, pp.31-34, 2003.
DOI : 10.1023/B:JARS.0000021015.15794.82
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.647

S. Seo, H. Yang, K. Yi, and T. Han, Goal-directed weakening of abstract interpretation results, ACM Transactions on Programming Languages and Systems, vol.29, issue.6, p.39, 2007.
DOI : 10.1145/1286821.1286830