EasyChair Publications
Search
Paper Information
Paper:Jasmin Christian Blanchette
Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod
Title:Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod
Authors:Jasmin Christian Blanchette
Keyphrases:counterexample generation, interactive theorem proving, model finding, higher order logic
Paper:
Abstract: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. 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.
Volume:Andrei Voronkov, Geoff Sutcliffe, Matthias Baaz and Christian Fermüller (editors). LPAR-17-short. short papers for 17th International Conference on Logic for Programming, Artificial intelligence, and Reasoning.
Series:EPiC Series in Computing
Volume number:13
Pages:20-25
Editors:Andrei Voronkov, Geoff Sutcliffe, Matthias Baaz and Christian Fermüller
Page views:26
Downloads:16
BibTeX entry:
@inproceedings{LPAR-17-short:Nitpick_A_Counterexample_Generator_for_Isabelle_HOL_Based_on_the_Relational_Model_Finder_Kodkod,
  author    = {Jasmin Christian Blanchette},
  title     = {Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod},
  booktitle = {LPAR-17-short. short papers for 17th International Conference on Logic for Programming, Artificial intelligence, and Reasoning.},
  editor    = {Andrei Voronkov and Geoff Sutcliffe and Matthias Baaz and Christian Ferm\verb=\="uller},
  series    = {EPiC Series in Computing},
  volume    = {13},
  pages     = {20-25},
  year      = {2013},
  publisher = {EasyChair},
  bibsource = {EasyChair, http://www.easychair.org},
  issn      = {2398-7340}}