Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL
No abstract available.
Related papers
- Towards verifying ethereum smart contract bytecode in Isabelle/HOL CPP 2018
- IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL TACAS 2024
- A machine-checked model for a Java-like language, virtual machine, and compiler TOPLAS 2006
- A verified prover based on ordered resolution CPP 2019
- IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL ECOOP 2025
- Javalight is Type-Safe - Definitely POPL 1998
- A Formal Framework for the Java Bytecode Language and Verifier OOPSLA 1999
- Verifying Term Graph Optimizations using Isabelle/HOL CPP 2023