Formalizing a JVML Verifier for Initialization in a Theorem Prover

This publication has 14 references indexed in Scilit:

• A Formal Executable Semantics of the JavaCard Platform
  Published by Springer Nature ,2001
• A formal framework for the Java bytecode language and verifier
  Published by Association for Computing Machinery (ACM) ,1999
• Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL
  Published by Springer Nature ,1999
• A Formal Specification of Javaℳ Virtual Machine Instructions for Objects, Methods and Subroutines
  Published by Springer Nature ,1999
• A specification of Java loading and bytecode verification
  Published by Association for Computing Machinery (ACM) ,1998
• Reasoning about classes in object-oriented languages: Logical models and tools
  Published by Springer Nature ,1998
• Formal verification for fault-tolerant architectures: prolegomena to the design of PVS
  IEEE Transactions on Software Engineering, 1995
• Isabelle
  Published by Springer Nature ,1994
• Synthesis of ML programs in the system Coq
  Journal of Symbolic Computation, 1993
• A unified approach to global program optimization
  Published by Association for Computing Machinery (ACM) ,1973