@inproceedings{BeckertKlevanovBormer2009,
  author =    {Bernhard Beckert and Thorsten Bormer and Vladimir Klebanov},
  title =     {On Essential Program Annotations and 
               Completeness of Verifying Compilers},
  booktitle = {Proceedings, Workshop on Verified Software: Theory, Tools, 
               and Experiments (VSTTE)},
  editors =   {Jean-Christophe Filli{\^a}tre and Leo Freitas},
  year =      {2009}
}