@InProceedings{KleinW-TPHOLS03,
  author =       {Gerwin Klein and Martin Wildmoser},
  title =        {Verified Bytecode Subroutines},
  booktitle =    {Proceedings of Theorem Proving in Higher Order Logics},
  pages =        {55--70},
  year =         {2003},
  editor =       {David Basin and Burkhard Wolff},
  volume =       {2758},
  series =       {Lecture Notes in Computer Science},
  url =          {\url{http://www4.in.tum.de/~kleing/papers/KleinW-TPHOLS03.html}}
}