Nitpick is an open source counterexample generator for Isabelle/HOL that is designed to handle formulas combining
(co)inductive datatypes, (co)inductively defined predicates, and (co)recursive functions. It
builds on Kodkod, a highly optimized first-order relational
model finder developed by the Software Design Group at
MIT. The name Nitpick is appropriated from a now retired Alloy
Nitrox is the first-order logic version of Nitpick. The name is a combination of
Nitpick and Paradox. Nitrox is little more
than a TPTP FOF parser on top of Nitpick.
Nitpick is integrated with the Thousands of Problems for Theorem Provers (TPTP)
and can be run remotely via the SystemOnTPTP
service. Two flavors are available:
- Nitpick: Nitpick for TPTP THF (the higher-order division)
- Nitrox: Nitpick for TPTP FOF/CNF (the first-order division)
Nitpicking C++ concurrency
J. C. B., Tjark Weber, Mark Batty, Scott Owens, and Susmit Sarkar.
13th International ACM SIGPLAN Symposium on
Principles and Practice of Declarative Programming (PPDP 2011),
pp. 113–124, ACM Press, 2011.
Automatic proof and disproof in Isabelle/HOL
J. C. B., Lukas Bulwahn, and Tobias Nipkow. In Tinelli, C., Sofronie-Stokkermans, V. (eds.) 8th International Symposium
Frontiers of Combining Systems (FroCoS 2011),
LNAI 6989, pp. 12–27, Springer, 2011.
Nitpick is part of Isabelle starting with version 2009-1. It can be
invoked using the nitpick command at any point in a proof.
For the benefit of software archaeologists, historical versions
of Nitpick are available below. These require Isabelle version 2009.
1.2.3 (12 Nov. 2009) ·
1.2.2 (16 Oct. 2009) ·
1.2.1 (25 Sept. 2009) ·
1.2.0 (27 July 2009) ·
1.1.1 (24 June 2009) ·
1.1.0 (16 June 2009) ·
1.0.3 (17 March 2009) ·
1.0.2 (12 March 2009) ·
1.0.1 (6 March 2009) ·
1.0.0 (27 Feb. 2009)
Nitrox (Nitpick for TPTP FOF/CNF) can be downloaded below:
0.2 (2 Sept. 2010) ·
0.1 (21 July 2010)
Nitpick would have been impossible without the help and support from Tobias
Nipkow and the members of the Isabelle group in Munich. Tjark Weber's pioneering
tool Refute guided the design of Nitpick. Alexander Krauss contributed to the
monotonicity inference calculi described in the IJCAR 2010 paper, and Koen
Claessen came up with the nonstandard model search presented at LPAR
Yogyakarta 2010. Emina Torlak developed the wonderful Kodkod model finder upon
which Nitpick is built. Geoff Sutcliffe installed Nitpick and Nitrox on his
Miami computer farm and runs them regularly against Refute, Satallax, Paradox,
and other model finders. Andreas Lochbihler, Denis Lohner, and Daniel Wasserrab
were among the first users of the system and provided much helpful feedback.
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber made the
C++ memory model case study possible. Sincere thanks to all of them (and to many
Jasmin Christian Blanchette
Fakultät für Informatik
Technische Universität München
blanchette0in.tum.de (substitute @ for 0)