[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