Sciweavers

Share
ITP
2010

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

9 years 2 months ago
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.
Jasmin Christian Blanchette, Tobias Nipkow
Added 15 Aug 2010
Updated 15 Aug 2010
Type Conference
Year 2010
Where ITP
Authors Jasmin Christian Blanchette, Tobias Nipkow
Comments (0)
books