I am pleased to announce the first release of Nitpick, a Kodkod (Alloy) based counterexample generator for Isabelle/HOL on which I've been working since October. (The name Nitpick is shamelessly stolen from an obsolete MIT tool.) The tool is similar to Refute in principle but it scales better and produces more genuine counterexamples for inductive datatypes.
You can download Nitpick from http://www4.in.tum.de/~blanchet/nitpick-1.0.0.tgz It requires a recent snapshot of Isabelle2009. The package contains everything you need: Nitpick (.thy + SML), Kodkod (Java), and a SAT solver (Java). To install it, just type './build'. The manual is included in the package and is also available at http://www4.in.tum.de/~blanchet/nitpick-1.0.0/Nitpick/Manual/nitpick.pdf The plan is to release Nitpick 1.1 to the wider public alongside the Isabelle2009 "winter" release, and then to incorporate it directly in Isabelle from then on. Please let me know if you have any feedback or bug reports concerning Nitpick, or if you find typos in the manual. Thanks, Jasmin
