G. Barthe, C. Kunz, D. Pichardie, and J. Samborski-forlese, Preservation of proof obligations for hybrid verification methods, Proc. of SEFM 2008, pp.127-136, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00332718

F. Besson, T. Jensen, and D. Pichardie, Proof-carrying code from certified abstract interpretation and fixpoint compression, Theoretical Computer Science, vol.364, issue.3, pp.273-291, 2006.
DOI : 10.1016/j.tcs.2006.08.012

M. G. Burke, J. Choi, S. Fink, D. Grove, M. Hind et al., The Jalape??o dynamic optimizing compiler for Java, Proceedings of the ACM 1999 conference on Java Grande , JAVA '99, pp.129-141, 1999.
DOI : 10.1145/304065.304113

T. Cramer, R. Friedman, T. Miller, D. Seberger, R. Wilson et al., Compiling Java just in time, IEEE Micro, vol.17, issue.3, pp.36-43, 1997.
DOI : 10.1109/40.591653

D. Demange, T. Jensen, and D. Pichardie, A Provably Correct Stackless Intermediate Representation for Java Bytecode, Research Report, vol.7021, 2009.
DOI : 10.1007/978-3-642-17164-2_8

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

N. Stephen, J. C. Freund, and . Mitchell, The type system for object initialization in the Java bytecode language, ACM TOPLAS, vol.21, issue.6, pp.1196-1250, 1999.

G. Klein and T. Nipkow, A machine-checked model for a Java-like language, virtual machine, and compiler, ACM Transactions on Programming Languages and Systems, vol.28, issue.4, pp.619-695, 2006.
DOI : 10.1145/1146809.1146811

F. Logozzo and M. Fähndrich, On the Relative Completeness of Bytecode Analysis Versus Source Code Analysis, Proc. of CC 2008, pp.197-212, 2008.
DOI : 10.1007/978-3-540-78791-4_14

Y. Matsuno and A. Ohori, A type system equivalent to static single assignment, Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming , PPDP '06, pp.249-260, 2006.
DOI : 10.1145/1140335.1140365

T. Jikes and R. Project, Jikes rvm -home page

E. Rose, Lightweight Bytecode Verification, Journal of Automated Reasoning, vol.31, issue.3/4, pp.303-334, 2003.
DOI : 10.1023/B:JARS.0000021015.15794.82

R. F. Stark, E. Borger, and J. Schmid, Java and the Java Virtual Machine: Definition, Verification , Validation with Cdrom, 2001.
DOI : 10.1007/978-3-642-59495-3

M. Strecker, Formal Verification of a Java Compiler in Isabelle, Proc. of CADE-18, pp.63-77, 2002.
DOI : 10.1007/3-540-45620-1_5

R. Vallée-rai, P. Co, E. Gagnon, L. Hendren, P. Lam et al., Soot -a Java bytecode optimization framework, Proc. of CASCON '99, 1999.

R. Vallee-rai and L. J. Hendren, Jimple: Simplifying Java bytecode for analyses and transformations, 1998.

J. Whaley, Dynamic optimization through the use of automatic runtime specialization. Master's thesis, Massachusetts Institute of Technology, 1999.

M. Wildmoser, A. Chaieb, and T. Nipkow, Bytecode Analysis for Proof Carrying Code, Proc. of BYTECODE 2005, 2005.
DOI : 10.1016/j.entcs.2005.02.040

H. Xi and S. Xia, Towards array bound check elimination in Java tm virtual machine language, Proc. of CASCON '99, p.14, 1999.