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.

Documentation

• Picking Nits: A User's Guide to Nitpick for Isabelle/HOL
  J. C. B.

  The above manual is for the latest official Isabelle release. If you use the latest Isabelle snapshot, you can invoke the up-to-date Nitpick documentation using the command isabelle doc nitpick.

TPTP Integration

Nitpick is integrated with the Thousands of Problems for Theorem Provers (TPTP) and can be run remotely via the SystemOnTPTP service, where it is called Nitrox for historical reasons.

Main Papers

• Nitpick: A counterexample generator for higher-order logic based on a relational model finder
  J. C. B. and Tobias Nipkow. In Kaufmann, M., Paulson, L. C. (eds.) First International Conference on Interactive Theorem Proving (ITP 2010), LNCS 6172, pp. 131–146, Springer, 2010.

• Relational analysis of (co)inductive predicates, (co)inductive datatypes, and (co)recursive functions
  J. C. B. To appear in a special issue of the Software Quality Journal.

• Monotonicity inference for higher-order logic
  J. C. B. and Alexander Krauss. Journal of Automated Reasoning 47(4), pp. 369–398, Dec. 2011.

• Generating counterexamples for structural inductions by exploiting nonstandard models
  J. C. B. and Koen Claessen. In Fermüller, C. G., Voronkov, A. (eds.) 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR Yogyakarta 2010), LNAI 6397, pp. 117–141, Springer, 2010.

• 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

• Nitpick: A counterexample generator for higher-order logic based on a relational model finder (extended abstract)
  J. C. B. and Tobias Nipkow. Third International Conference on Tests and Proofs (TAP 2009). In Dubois, C. (ed.) TAP 2009: Short Papers, ETH Technical Report 630, July 2009.

• Nitpick: A counterexample generator for Isabelle/HOL based on the relational model finder Kodkod (system description)
  J. C. B. Presented at the 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR Yogyakarta 2010).

• Relational analysis of (co)inductive predicates, (co)inductive datatypes, and (co)recursive functions
  J. C. B. In Fraser, G., Gargantini, A. (eds.) Fourth International Conference on Tests and Proofs (TAP 2010), LNCS 6143, pp. 117–134, Springer, 2010.

• Monotonicity inference for higher-order logic
  J. C. B. and Alexander Krauss. In Giesl, J., Hähnle, R. (eds.) 5th International Joint Conference on Automated Reasoning (IJCAR 2010), LNCS 6173, pp. 91–106, Springer, 2010.

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

Historical versions of 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)