@InProceedings{Fontaine8,
  author =       "Pascal Fontaine and Jean-Yves Marion and Stephan Merz
                 and Leonor Prensa Nieto and Alwen Tiu",
  title =        "Expressiveness + Automation + Soundness: Towards
                 Combining {SMT} Solvers and Interactive Proof
                 Assistants",
  booktitle =    tacas,
  editor =       "Holger Hermanns and Jens Palsberg",
  year =         "2006",
  pages =        "167--181",
  series =       "Lecture Notes in Computer Science",
  publisher =    "Springer-Verlag",
  volume =       "3920",
}