G. [. Barthe and . Dufay, A Tool-Assisted Framework for??Certified??Bytecode??Verification, Proc. of FASE'04, pp.99-113, 2004.
DOI : 10.1007/978-3-540-24721-0_7

G. Barthe, G. Dufay, M. Huisman, S. Melo, and . Sousa, Jakarta: A Toolset for Reasoning about JavaCard, Proc. of e-SMART'01. Springer LNCS, 2001.
DOI : 10.1007/3-540-45418-7_2

. Bdj-+-01-]-g, G. Barthe, L. Dufay, B. Jakubiec, S. Serpette et al., A formal executable semantics of the JavaCard platform, Proc. ESOP'01, number 2028 in LNCS, 2001.

Y. Bertot-bertot, B. Grégoire, X. [. Leroy, R. Cousot, . [. Cousot et al., A structured approach to proving compiler optimizations based on dataflow analysis Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints Systematic design of program analysis frameworks Abstract interpretation and application to logic programs, LERNET Summer School Proc. of TYPES'04 Proc. of POPL'77 Proc. of POPL'79CC92b] P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, pp.66-81, 1977.

S. Coupet-grimal and W. Delobel, A Uniform and Certified Approach for Two Static Analyses, Proc. of TYPES'04, pp.115-137, 2006.
DOI : 10.1007/11617990_8

D. Cachera, T. Jensen, D. Pichardie, and V. Rusu, Extracting a data flow analyser in constructive logic, Theoretical Computer Science, vol.342, issue.1, pp.56-78, 2005.
DOI : 10.1016/j.tcs.2005.06.004

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

T. [. Cachera, D. Jensen, G. Pichardie, . [. Schneider, T. Klein et al., Certified Memory Usage Analysis Coq development team. The Coq proof assistant reference manual V8.2 The calculational design of a generic abstract interpreter Verified Bytecode Verifiers A machine-checked model for a Java-like language , virtual machine and compiler Towards a mechanized metatheory of standard ml [Ler06] X. Leroy. Formal certification of a compiler back-end or: programming a compiler with a proof assistant Securing Java: getting down to business with mobile code, Proc ? of FM'05 Calculational System Design. NATO ASI Series F. IOS Press Proc. of POPL'07 Proc. of POPL'06Mon98] D. Monniaux. Réalisation mécanisée d'interpréteurs abstraits french. [Pic08] D. Pichardie. Building certified static analysers by modular construction of well-founded lattices Proc. of FICS'08 of Electronic Notes in Theoretical Computer Science, pp.91-106583, 1998.
DOI : 10.1007/11526841_8

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