@article{KleinW-JAR03,
  author =  {Gerwin Klein and Martin Wildmoser},
  title =   {Verified Bytecode Subroutines},
  journal = {Journal of Automated Reasoning},
  year =    2003,
  volume = 30,
  number = {3--4},
  pages = {363--398},
  editor = {Tobias Nipkow},
  url =     {\url{http://www4.in.tum.de/~kleing/papers/KleinW-JAR02.html}}
}