Asserting Bytecode Safety
Abstract elided by the publisher.
Related papers
- JayHorn: A Java Model Checker - (Competition Contribution) TACAS 2019
- JBMC: Bounded Model Checking for Java Bytecode - (Competition Contribution) TACAS 2019
- Hevm, a Fast Symbolic Execution Framework for EVM Bytecode CAV 2024
- Java bytecode verification via static single assignment form TOPLAS 2008
- Towards verifying ethereum smart contract bytecode in Isabelle/HOL CPP 2018
- Miniboxing: improving the speed to code size tradeoff in parametric polymorphism translations OOPSLA 2013
- 2LS: Memory Safety and Non-termination - (Competition Contribution) TACAS 2018
- A machine-checked model for a Java-like language, virtual machine, and compiler TOPLAS 2006