G. Barthe, G. Dufay, L. Jakubiec, S. Melo, and . Sousa, A formal correspondence between offensive and defensive javacard virtual machines. In VMCAI '02: Revised Papers from the Third International Workshop on Verification , Model Checking, and Abstract Interpretation Small witnesses for abstract interpretation-based proofs, ESOP '07: Proceedings of the 16th European Symposium on Programming, 2002.
DOI : 10.1007/3-540-47813-2_3

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.7.9616

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, 1977.
DOI : 10.1145/512950.512973

URL : https://hal.archives-ouvertes.fr/inria-00528590

A. Brian, H. A. Davey, and . Priestley, Introduction to Lattices and Order, 1990.

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

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

G. Klein, Verified Java Bytecode Verification, 2003.

B. Todd, J. Knoblock, and . Rehof, Type elaboration and subtype completion for java bytecode, In ACM Transations on Programming Languages and Systems, vol.23, issue.2, 2001.

X. Leroy, Java bytecode verification: algorithms and formalizations, Journal of Automated Reasoning, vol.30, issue.3, 2003.
URL : https://hal.archives-ouvertes.fr/hal-01499939

X. Leroy and F. Rouaix, Security properties of typed applets, POPL '98: Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, 1998.
URL : https://hal.archives-ouvertes.fr/hal-01499957

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

C. George and . Necula, Proof-carrying code, POPL '97: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of programming languages, 1997.

C. Pusch, Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL, TACAS '99: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, 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, 1999.

Z. Qian, Standard fixpoint iteration for Java bytecode verification, ACM Transactions on Programming Languages and Systems, vol.22, issue.4, 2000.
DOI : 10.1145/363911.363915

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.1730

[. Rose, Lightweight Bytecode Verification, Journal of Automated Reasoning, vol.31, issue.3/4, 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, 2007.
DOI : 10.1145/1286821.1286830