G. Barthe, G. Dufay, M. Huisman, S. Melo, and . Sousa, Jakarta: A Toolset for Reasoning about JavaCard, Proc. e-SMART'01, number 2140 in Lecture Notes in Computer Science, 2001.
DOI : 10.1007/3-540-45418-7_2

G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, S. Melo et al., A Formal Executable Semantics of the JavaCard Platform, Proc. ESOP'01, number 2028 in Lecture Notes in Computer Science, 2001.
DOI : 10.1007/3-540-45309-1_20

Y. Bertot, Formalizing a JVML Verifier for Initialization in a Theorem Prover, Proc. CAV'01, number 2102 in Lecture Notes in Computer Science, 2001.
DOI : 10.1007/3-540-44585-4_3

F. Besson, T. Jensen, D. L. Métayer, and T. Thorn, Model checking security properties of control flow graphs, Journal of Computer Security, vol.9, issue.3, pp.217-250, 2001.
DOI : 10.3233/JCS-2001-9303

D. Cachera, T. Jensen, D. Pichardie, and V. Rusu, Extracting a data flow analyser in constructive logic, Proc. ESOP'04, number 2986 in Lecture Notes in Computer Science, pp.385-400, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00564633

L. Casset, L. Burdy, and A. Requet, Formal development of an embedded verifier for Java Card byte code, Proceedings International Conference on Dependable Systems and Networks, 2002.
DOI : 10.1109/DSN.2002.1028886

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

X. Leroy, French ARC Concert research project : compilateurs certifiés

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

E. Denney, The synthesis of a Java card tokenisation algorithm, Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001), pp.43-50, 2001.
DOI : 10.1109/ASE.2001.989789

T. Genet, T. Jensen, V. Kodati, and D. Pichardie, A Java Card CAP converter in PVS, Proc. of 2nd International Workshop on Compiler Optimization Meets Compiler Verification, 2003.

R. Hansen, Flow Logic for Carmel, 2002.

G. Klein and T. Nipkow, Verified bytecode verifiers, Theoretical Computer Science, vol.298, issue.3, pp.583-626, 2002.
DOI : 10.1016/S0304-3975(02)00869-1

S. Lerner, T. Millstein, and C. Chambers, Automatically proving the correctness of compiler optimizations, Proc. of the ACM SIGPLAN 2003 conference on Programming language design and implementation, pp.220-231, 2003.

R. Marlet, Syntax of the JCVM language to be studied in the SecSafe project, 2001.

D. Monniaux, Réalisation mécanisée d'interpréteurs abstraits, 1998.

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

H. Nielson and F. Nielson, Flow logics for constraint based analysis, Proc. CC'98, number 1383 in Lecture Notes in Computer Science, pp.109-127, 1998.
DOI : 10.1007/BFb0026426

C. Okasaki and A. Gill, Fast mergeable integer maps, Proc. of the ACM SIGPLAN Workshop on ML, pp.77-86, 1998.

]. Pichardie, Coq sources of the development

F. Prost, Interprétation de l'analyse statique en théorie des types, 1999.

I. Siveroni, Operational semantics of the Java Card Virtual Machine, The Journal of Logic and Algebraic Programming, vol.58, issue.1-2, pp.3-25, 2004.
DOI : 10.1016/j.jlap.2003.07.003