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.


References in zbMATH (referenced in 21 articles , 1 standard article )

Showing results 1 to 20 of 21.
Sorted by year (citations)

1 2 next

  1. Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno: Computer-assisted analysis of the Anderson-Hájek ontological controversy (2017)
  2. Reynolds, Andrew; Blanchette, Jasmin Christian: A decision procedure for (co)datatypes in SMT solvers (2017)
  3. Guttmann, Walter: An algebraic approach to computations with progress (2016)
  4. 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)
  5. Raggi, Daniel; Bundy, Alan; Grov, Gudmund; Pease, Alison: Automating change of representation for proofs in discrete mathematics (extended version) (2016)
  6. Berghammer, Rudolf; Guttmann, Walter: Closure, properties and closure properties of multirelations (2015)
  7. Foster, Simon; Struth, Georg: On the fine-structure of regular algebra (2015)
  8. Guttmann, Walter: Infinite executions of lazy and strict computations (2015)
  9. Raggi, Daniel; Bundy, Alan; Grov, Gudmund; Pease, Alison: Automating change of representation for proofs in discrete mathematics (2015)
  10. Reynolds, Andrew; Blanchette, Jasmin Christian: A decision procedure for (co)datatypes in SMT solvers (2015)
  11. Benzmüller, Christoph; Paulson, Lawrence C.: Quantified multimodal logics in simple type theory (2013)
  12. Foster, Simon; Woodcock, Jim: Unifying theories of programming in Isabelle (2013)
  13. Bulwahn, Lukas: The new quickcheck for isabelle. Random, exhaustive and symbolic testing under one roof (2012)
  14. Guttmann, Walter: Algebras for iteration and infinite computations (2012)
  15. Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias: Automatic proof and disproof in Isabelle/HOL (2011)
  16. Blanchette, Jasmin Christian; Krauss, Alexander: Monotonicity inference for higher-order formulas (2011)
  17. Benzmüller, Christoph: Verifying the modal logic cube is an easy task (for higher-order automated reasoners) (2010)
  18. Blanchette, Jasmin Christian; Claessen, Koen: Generating counterexamples for structural inductions by exploiting nonstandard models (2010)
  19. Blanchette, Jasmin Christian; Krauss, Alexander: Monotonicity inference for higher-order formulas (2010)
  20. Blanchette, Jasmin Christian; Nipkow, Tobias: Nitpick: a counterexample generator for higher-order logic based on a relational model finder (2010)

1 2 next