Nitpick: A Counterexample Generator for Higher-Order
Logic Based on a Relational Model Finder
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}