@article{KleinN-CCPE01,
  author = {Gerwin Klein and Tobias Nipkow},
  title = {Verified Lightweight Bytecode Verification},
  journal = {Concurrency and Computation: Practice and Experience},
  editor = {S. Eisenbach and G. T. Leavens},
  publisher = {John Wiley and Sons},
  volume = 13,
  number = 13,
  pages = {1133-1151},
  year = 2001,
  url = {\url{http://www4.in.tum.de/~kleing/papers/cpe01.html}}
}