[Club2] Dry run -- Indonesia
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Fri Sep 3 14:10:29 CEST 2010
Am 03.09.2010 um 14:08 schrieb Jasmin Christian Blanchette:
> Wed Sept. 29, 14:00, Turing (00.09.055)
> Nitpick: A Counterexample Generator for Isabelle/HOL Based on the Relational Model Finder Kodkod
> (System Description; LPAR)
>
> 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.
>
> ---
>
> Wed Sept. 29, 14:00, Turing (00.09.055)
Copy paste mistake: It should read "Oct. 6, 14:00, Turing".
Jasmin
More information about the Club2
mailing list