Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder

Jasmin Christian Blanchette and Tobias Nipkow

Nitpick is a counterexample generator for Isabelle/HOL that builds on Kodkod, a SAT-based first-order relational model finder. Nitpick supports unbounded quantification, (co)inductive predicates and datatypes, and (co)recursive functions. Fundamentally a finite model finder, it approximates infinite types by finite subsets. As case studies, we consider a security type system and a hotel key card system. Our experimental results on Isabelle theories and the TPTP library indicate that Nitpick generates more counterexamples than other model finders for higher-order logic, without restrictions on the form of the formulas to falsify.

pdf

BibTeX:

@inproceedings{BlanchetteN-ITP10,
author={Jasmin Christian Blanchette and Tobias Nipkow},
title={Nitpick: A ounterexample generator for higher-order logic based on a relational model finder},
booktitle={Interactive Theorem Proving (ITP 2010)},
editor={M. Kaufmann and L. Paulson},
publisher=Springer,series=LNCS,volume={6172},pages={131-146},year=2010}