@inproceedings{VSchuppanABiere-TACAS-2005,
  author   = {Viktor Schuppan and Armin Biere},
  title    = {Shortest Counterexamples for Symbolic Model Checking of {LTL} with Past},
  pages    = {493--509},
  crossref = {conf/tacas/2005},
  ee       = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3440&spage=493}
}

@proceedings{conf/tacas/2005,
  editor    = {Nicolas Halbwachs and Lenore D. Zuck},
  title     = {Tools and Algorithms for the Construction and Analysis of Systems: 11th International Conference, TACAS 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4--8, 2005. Proceedings},
  booktitle = {TACAS'05},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3440},
  year      = {2005},
  isbn      = {3-540-25333-5},
}