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.

• Type: Conference
• Year: 2010
• Where: ITP
• Authors: Jasmin Christian Blanchette, Tobias Nipkow
• Keywords: Hotel Key Card, ITP 2010, Mathematics, Model finders, first-order Relational Model