Verified Lightweight Bytecode Verification

Gerwin Klein and Tobias Nipkow

Eva and Kristoffer Rose proposed a (sparse) annotation of Java Virtual Machine code with types to enable a one-pass verification of welltypedness. We have formalized a variant of their proposal in the theorem prover Isabelle/HOL and proved soundness and completeness.

pdf ps


@article{KleinN-CCPE,author={Gerwin Klein and Tobias Nipkow},
title={Verified Lightweight Bytecode Verification},
journal={Concurrency and Computation: Practice and Experience},
Journal page