@inproceedings{KleinN00,
author={Gerwin Klein and Tobias Nipkow},
title={Verified Lightweight Bytecode Verification},
booktitle = {Formal Techniques for {J}ava Programs},
year = {2000},
publisher = {Fernuniversit{{\"a}t} Hagen},
editor = {Drossopoulou, S. and Eisenbach, S. and Jacobs, B. and Leavens, G. T. and M{\"u}ller, P. and Poetzsch-Heffter, A.},
organization = {Technical Report 269, 5/2000, Fernuniversit{{\"a}t} Hagen},
note = {ECOOP2000 Workshop proceedings available from \url{http://www.informatik.fernuni-hagen.de/pi5/publications.html}},
url  = {\url{http://www4.in.tum.de/~nipkow/pubs/lbv.html}}
}