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
Jakarta: A Toolset for Reasoning about JavaCard, Proc. of e-SMART'01. Springer LNCS, 2001. ,
DOI : 10.1007/3-540-45418-7_2
A formal executable semantics of the JavaCard platform, Proc. ESOP'01, number 2028 in LNCS, 2001. ,
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. ,
A Uniform and Certified Approach for Two Static Analyses, Proc. of TYPES'04, pp.115-137, 2006. ,
DOI : 10.1007/11617990_8
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
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