A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines, Proc. of the 3rd Int. Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI'02), pp.32-45, 2002. ,
DOI : 10.1007/3-540-47813-2_3
Computing Stack Maps with Interfaces, 2007. ,
DOI : 10.1007/978-3-540-70592-5_27
URL : https://hal.archives-ouvertes.fr/inria-00332526
Small witnesses for abstract interpretationbased proofs, Proc. of the 16th European Symp. on Programming, pp.268-283, 2007. ,
CLDC Byte Code Typechecker Specification, 2003. ,
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
Introduction to Lattices and Order, 1990. ,
DOI : 10.1017/CBO9780511809088
A type system for the java bytecode language and verifier, Journal of Automated Reasoning, vol.30, pp.3-4271, 2003. ,
A specification of Java loading and bytecode verification, Proceedings of the 5th ACM conference on Computer and communications security , CCS '98, pp.49-58, 1998. ,
DOI : 10.1145/288090.288104
Type elaboration and subtype completion for Java bytecode, ACM Transactions on Programming Languages and Systems, vol.23, issue.2, pp.243-272, 2001. ,
DOI : 10.1145/383043.383045
Java bytecode verification: algorithms and formalizations, Journal of Automated Reasoning, vol.30, issue.3/4, pp.235-269, 2003. ,
DOI : 10.1023/A:1025055424017
URL : https://hal.archives-ouvertes.fr/hal-01499939
Security properties of typed applets, Proc. of the 25th ACM Symp. on Principles of Programming Languages (POPL'98), pp.391-403, 1998. ,
URL : https://hal.archives-ouvertes.fr/hal-01499957
The Java Virtual Machine Specification, 1999. ,
Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL, Proc. of the 5th Int. Conf. on Tools and Algorithms for Construction and Analysis of Systems (TACAS'99), pp.89-103, 1999. ,
DOI : 10.1007/3-540-49059-0_7
A formal specification of java virtual machine instructions for objects, methods and subrountines. Formal Syntax and Semantics of Java, pp.271-312, 1999. ,
Lightweight Bytecode Verification, Journal of Automated Reasoning, vol.31, issue.3/4, pp.31-34, 2003. ,
DOI : 10.1023/B:JARS.0000021015.15794.82
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.647
Goal-directed weakening of abstract interpretation results, ACM Transactions on Programming Languages and Systems, vol.29, issue.6, p.39, 2007. ,
DOI : 10.1145/1286821.1286830