[Club2] Nitpick -- Yet another counterexample generator for Isabelle/HOL
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Mon Jan 12 13:52:15 CET 2009
Nitpick ist ein neuer Gegenbeispielgenerator für Isabelle/HOL, den ich
seit Oktober über die Kodkod-Bibliothek [1] entwickle. Das Werkzeug
ist noch in Entwicklung, allerdings scheint mir die Zeit reif für eine
Einfürung, in der ich sowohl die Kodkod-Logik als auch meine HOL-nach-
Kodkod-Übersetzung erklären kann. Ich schlage folgenden Zeitpunkt vor:
Mittwoch 21-Jan-2008, 14:00 bis 15:00
Raum 00.09.055 (Turing)
Jasmin
[1] http://alloy.mit.edu/kodkod/
More information about the Club2
mailing list