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

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

1 2 3 4 next

  1. Dubut, Jérémy; Yamada, Akihisa: Fixed points theorems for non-transitive relations (2022)
  2. Lewis, Robert Y.; Wu, Minchao: A bi-directional extensible interface between Lean and Mathematica (2022)
  3. Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
  4. Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
  5. Benzmüller, Christoph; Fuenmayor, David: Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel’s ontological argument (2020)
  6. Benzmüller, Christoph; Parent, Xavier; van der Torre, Leendert: Designing normative theories for ethical and legal reasoning: \textscLogiKEyframework, methodology, and tool support (2020)
  7. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  8. Fuenmayor, David; Benzmüller, Christoph: Computational hermeneutics: an integrated approach for the logical analysis of natural-language arguments (2019)
  9. Fuenmayor, David; Benzmüller, Christoph: Mechanised assessment of complex natural-language arguments using expressive logic combinations (2019)
  10. Kaliszyk, Cezary; Pąk, Karol: Semantics of Mizar as an Isabelle object logic (2019)
  11. Milicevic, Aleksandar; Near, Joseph P.; Kang, Eunsuk; Jackson, Daniel: Alloy*: a general-purpose higher-order relational constraint solver (2019)
  12. Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
  13. Abdulaziz, Mohammad; Norrish, Michael; Gretton, Charles: Formally verified algorithms for upper-bounding state space diameters (2018)
  14. 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)
  15. Benzmüller, Christoph; Farjami, Ali; Parent, Xavier: A dyadic deontic logic in HOL (2018)
  16. Benzmüller, Christoph; Parent, Xavier; van der Torre, Leendert: A deontic logic reasoning infrastructure (2018)
  17. Dailler, Sylvain; Hauzar, David; Marché, Claude; Moy, Yannick: Instrumenting a weakest precondition calculus for counterexample generation (2018)
  18. Dubois, Catherine; Giorgetti, Alain: Tests and proofs for custom data generators (2018)
  19. Guttmann, Walter: Verifying minimum spanning tree algorithms with Stone relation algebras (2018)
  20. Lochbihler, Andreas: Mechanising a type-safe model of multithreaded Java with a verified compiler (2018)

1 2 3 4 next