A B model for ensuring soundness of a large subset of the Java Card virtual machine
- 31 March 2003
- journal article
- Published by Elsevier in Science of Computer Programming
- Vol. 46 (3) , 283-306
- https://doi.org/10.1016/s0167-6423(02)00095-3
Abstract
No abstract availableKeywords
This publication has 6 references indexed in Scilit:
- Correctness of Java Card Method Lookup via Logical RelationsPublished by Springer Nature ,2000
- Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOLPublished by Springer Nature ,1999
- A specification of Java loading and bytecode verificationPublished by Association for Computing Machinery (ACM) ,1998
- A type system for object initialization in the Java bytecode languagePublished by Association for Computing Machinery (ACM) ,1998
- Byte code verification for Java smart cards based on model checkingPublished by Springer Nature ,1998
- Javalight is type-safe---definitelyPublished by Association for Computing Machinery (ACM) ,1998