@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{{\"a}t} Hagen},
  editor = {S. Drossopoulou and S. Eisenbach and B. Jacobs and 
            G. T. Leavens and P. M{\"u}ller and A. Poetzsch-Heffter},
  organization = {Technical Report 269},
  url  = {\url{http://www4.in.tum.de/~kleing/papers/lbv.html}}
}