Nitpick
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.
Keywords for this software
References in zbMATH (referenced in 35 articles , 1 standard article )
Showing results 1 to 20 of 35.
Sorted by year (- Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno: Computer-assisted analysis of the Anderson-Hájek ontological controversy (2017)
- Berghammer, Rudolf; Guttmann, Walter: An algebraic approach to multirelations and their properties (2017)
- Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel: A lambda-free higher-order recursive path order (2017)
- Cheney, James; Momigliano, Alberto: $\alpha\mathrmCheck$: a mechanized metatheory model checker (2017)
- Guttmann, Walter: Stone relation algebras (2017)
- Lampropoulos, Leonidas; Gallois-Wong, Diane; Hriţcu, Cătălin; Hughes, John; Pierce, Benjamin C.; Xia, Li-yao: Beginner’s Luck: a language for property-based generators (2017)
- Reynolds, Andrew; Blanchette, Jasmin Christian: A decision procedure for (co)datatypes in SMT solvers (2017)
- Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark: Constraint solving for finite model finding in SMT solvers (2017)
- Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam: Detecting inconsistencies in large first-order knowledge bases (2017)
- Dubois, Catherine; Giorgetti, Alain; Genestier, Richard: Tests and proofs for enumerative combinatorics (2016)
- Guttmann, Walter: An algebraic approach to computations with progress (2016)
- Ma, Sha; Shi, Zhiping; Shao, Zhenzhou; Guan, Yong; Li, Liming; Li, Yongdong: Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm (2016)
- Raggi, Daniel; Bundy, Alan; Grov, Gudmund; Pease, Alison: Automating change of representation for proofs in discrete mathematics (extended version) (2016)
- Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare: Model finding for recursive functions in SMT (2016)
- Steen, Alexander; Benzmüller, Christoph: Sweet SIXTEEN: automation via embedding into classical higher-order logic (2016)
- Wisniewski, Max; Steen, Alexander; Kern, Kim; Benzmüller, Christoph: Effective normalization techniques for HOL (2016)
- Benzmüller, Christoph: Invited talk: on a (quite) universal theorem proving approach and its application in metaphysics (2015)
- Benzmüller, Christoph; Woltzenlogel Paleo, Bruno: Higher-order modal logics: automation and applications (2015)
- Berghammer, Rudolf; Guttmann, Walter: Closure, properties and closure properties of multirelations (2015)
- Foster, Simon; Struth, Georg: On the fine-structure of regular algebra (2015)