and Nitrox

 

Description

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 precursor.
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.

Documentation

TPTP Integration

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)

Main Papers

  • 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.

Other Papers

  • 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.

Download

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)

Thanks

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 others)!

Contact

Jasmin Christian Blanchette
Fakultät für Informatik
Technische Universität München
blanchette0in.tum.de (substitute @ for 0)