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
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