[Club2] TAP/FLoC dry runs, updated schedule

[Jasmin Blanchette]

Hi all,

Because of the Aschewolke I had to change my vacation plans and reschedule my talks. Here is the new schedule:


TAP 2010
Relational Analysis of (Co)inductive Predicates, (Co)inductive Datatypes, and (Co)recursive Functions
http://www4.in.tum.de/~blanchet/tap2010-relational.pdf
Wed. May 12, 2010 at 14:00 in Turing (00.11.055)

This paper presents techniques for applying a finite relational model finder to logical specifications that involve (co)inductive predicates, (co)algebraic datatypes, and (co)recursive functions. In contrast to previous work, which focused on algebraic datatypes and restricted occurrences of unbounded quantifiers in formulas, we can handle arbitrary formulas by means of a three-valued Kleene logic. The techniques form the basis of the counterexample generator Nitpick for Isabelle/HOL. As a case study, we consider a coalgebraic lazy list type.


ITP-10
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
(joint work with Tobias)
http://www4.in.tum.de/~blanchet/itp2010-nitpick.pdf
Wed. May 26, 2010 at 14:00 in Turing (00.11.055)

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. As case studies, we consider a security type system and a hotel key card system. 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.


IJCAR 2010
Monotonicity Inference for Higher-Order Logic
(joint work with Alex)
http://www4.in.tum.de/~blanchet/ijcar2010-mono.pdf
Thu. June 3, 2010 at 14:00 in Turing (00.11.055)

Formulas are often monotonic in the sense that if the formula is satisfiable for given domains of discourse, it is also satisfiable for all larger domains. Monotonicity is undecidable in general, but we devised two calculi that infer it in many cases for higher-order logic. The stronger calculus has been implemented in Isabelle’s model finder Nitpick, where it is used to prune the search space, leading to dramatic speed improvements for formulas involving many atomic types.


I hope to see you there!

Cheers,

Jasmin