[Club2] Reminder: Talk at 14:00
Jasmin Blanchette
jasmin.blanchette at gmail.com
Wed Sep 22 10:08:05 CEST 2010
Hi all,
I will be rehearsing the following LPAR talk today:
Wed Sept. 22, 14:00, Zuse (01.11.018)
Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models
(with Koen Claessen)
http://www4.in.tum.de/~blanchet/lpar2010-nonstd.pdf
Induction proofs often fail because the stated theorem is noninductive, in which case the user must strengthen the theorem or prove auxiliary properties before performing the induction step. (Counter)model finders are useful for detecting non-theorems, but they will not find any counterexamples for noninductive theorems. We explain how to apply a well-known concept from first-order logic, nonstandard models, to the detection of noninductive invariants. Our work was done in the context of the proof assistant Isabelle/HOL and the counterexample generator Nitpick.
I hope to see you there!
Jasmin
More information about the Club2
mailing list