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.
@inproceedings{KleinN00,
author = {Gerwin Klein and Tobias Nipkow},
title = {Verified Lightweight Bytecode Verification},
booktitle = {Proc.\ 2nd {ECOOP} Workshop on Formal Techniques for {Java} Programs},
year = {2000},
publisher = {Fernuniversit{ät} Hagen},
editor = {S. Drossopoulou and S. Eisenbach and B. Jacobs and
G. T. Leavens and P. Müller and A. Poetzsch-Heffter},
organization = {Technical Report 269},
url = {\url{http://www4.in.tum.de/~kleing/papers/lbv.html}}
}