@InProceedings{Blanchette:ITP2010-131,
  author =       "Jasmin Christian Blanchette and Tobias Nipkow",
  title =        "{Nitpick}: {A} Counterexample Generator For Higher-Order
                 Logic Based on a Relational Model Finder",
  pages =        "131--146",
  ee =           "http://dx.doi.org/10.1007/978-3-642-14052-5_11",
  editor =       "Matt Kaufmann and Lawrence Paulson and Michael
                 Norrish",
  booktitle =    "Interactive Theorem Proving (ITP 2010)",
  address =      "Edinburgh, UK",
  year =         "2010",
  month =        jul,
  publisher =    "Springer",
  series =       "Lecture Notes in Computer Science",
  volume =       "6172",
}