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 46 articles , 1 standard article )

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

1 2 3 next

  1. Abdulaziz, Mohammad; Norrish, Michael; Gretton, Charles: Formally verified algorithms for upper-bounding state space diameters (2018)
  2. Avigad, Jeremy (ed.); Blanchette, Jasmin Christian (ed.); Klein, Gerwin (ed.); Paulson, Lawrence (ed.); Popescu, Andrei (ed.); Snelting, Gregor (ed.): Introduction to “Milestones in interactive theorem proving” (2018)
  3. Dailler, Sylvain; Hauzar, David; Marché, Claude; Moy, Yannick: Instrumenting a weakest precondition calculus for counterexample generation (2018)
  4. Dubois, Catherine; Giorgetti, Alain: Tests and proofs for custom data generators (2018)
  5. Guttmann, Walter: Verifying minimum spanning tree algorithms with Stone relation algebras (2018)
  6. Lochbihler, Andreas: Mechanising a type-safe model of multithreaded Java with a verified compiler (2018)
  7. Paulson, Lawrence C.: Computational logic: its origins and applications (2018)
  8. Schreiner, Wolfgang: Validating mathematical theorems and algorithms with RISCAL (2018)
  9. Benzmüller, C.; Weber, Leon; Woltzenlogel Paleo, Bruno: Computer-assisted analysis of the Anderson-Hájek ontological controversy (2017)
  10. Berghammer, Rudolf; Guttmann, Walter: An algebraic approach to multirelations and their properties (2017)
  11. Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy: Foundational (co)datatypes and (co)recursion for higher-order logic (2017)
  12. Blanchette, Jasmin Christian; Waldmann, Uwe; Wand, Daniel: A lambda-free higher-order recursive path order (2017)
  13. Cheney, James; Momigliano, Alberto: (\alpha\mathrmCheck): a mechanized metatheory model checker (2017)
  14. Guttmann, Walter: Stone relation algebras (2017)
  15. 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)
  16. Reynolds, Andrew; Blanchette, Jasmin Christian: A decision procedure for (co)datatypes in SMT solvers (2017)
  17. Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark: Constraint solving for finite model finding in SMT solvers (2017)
  18. Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam: Detecting inconsistencies in large first-order knowledge bases (2017)
  19. Dubois, Catherine; Giorgetti, Alain; Genestier, Richard: Tests and proofs for enumerative combinatorics (2016)
  20. Guttmann, Walter: An algebraic approach to computations with progress (2016)

1 2 3 next