Email Gateway (Aug 18 2022 at 13:36): Email Gateway (Aug 18 2022 at 13:36):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Dear all,
I am pleased to announce the release of the first stable version of
Nitpick. Nitpick 1.1 is a counterexample generator for Isabelle/HOL
2009 designed to cope with non-executable formulas (unlike
Quickcheck). It builds on the Alloy backend Kodkod, a highly optimized
first-order model finder developed by Daniel Jackson's group at MIT.
You can download Nitpick from
http://isabelle.in.tum.de/~blanchet/nitpick-1.1.tgz
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 available at
http://isabelle.in.tum.de/~blanchet/nitpick-1.1/Nitpick/manual/nitpick.pdf
If you plan on using Nitpick substantially, I strongly recommend you
download and compile MiniSat and set the MINISAT_HOME variable in your
"~/.isabelle/etc/settings" file to the directory that contains the
"minisat" executable (see section 5.5 of the manual).
I am looking forward to your feedback. In particular, I would like to
know if
1. the tool generated a spurious counterexample (it shouldn't, but
see section 7 of the manual);
2. the tool generated no counterexample for a non-theorem, and you
have reasons to believe it should have found one;
3. the tool raised an exception; or
4. you found a mistake in the documentation.
Regards,
Jasmin
Last updated: May 03 2024 at 08:18 UTC