Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL
- 12 March 1999
- book chapter
- Published by Springer Nature
Abstract
No abstract availableKeywords
This publication has 6 references indexed in Scilit:
- The Operational Semantics of a Java Secure ProcessorPublished by Springer Nature ,1999
- A Formal Specification of Javaℳ Virtual Machine Instructions for Objects, Methods and SubroutinesPublished by Springer Nature ,1999
- Machine-Checking the Java Specification: Proving Type-SafetyPublished by Springer Nature ,1999
- A type system for object initialization in the Java bytecode languagePublished by Association for Computing Machinery (ACM) ,1998
- A type system for Java bytecode subroutinesPublished by Association for Computing Machinery (ACM) ,1998
- IsabellePublished by Springer Nature ,1994