A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines

This publication has 15 references indexed in Scilit:

• Efficient Reasoning about Executable Specifications in Coq
  Published by Springer Nature ,2002
• Formalizing the safety of Java, the Java virtual machine, and Java card
  ACM Computing Surveys, 2001
• Jakarta: A Toolset for Reasoning about JavaCard
  Published by Springer Nature ,2001
• Formalizing a JVML Verifier for Initialization in a Theorem Prover
  Published by Springer Nature ,2001
• Abstract Interpretation Based Formal Methods and Future Challenges
  Published by Springer Nature ,2001
• Verified Bytecode Verifiers
  Published by Springer Nature ,2001
• A Formal Executable Semantics of the JavaCard Platform
  Published by Springer Nature ,2001
• Formal Proof of Smart Card Applets Correctness
  Published by Springer Nature ,2000
• A type system for object initialization in the Java bytecode language
  ACM Transactions on Programming Languages and Systems, 1999
• The B-Book
  Published by Cambridge University Press (CUP) ,1996