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

BibTeX:

@article{KleinN-CCPE,author={Gerwin Klein and Tobias Nipkow},
title={Verified Lightweight Bytecode Verification},
journal={Concurrency and Computation: Practice and Experience},
volume=13,pages={1133-1151},year=2001}

Journal page