[Club2] TAP/FLoC dry runs confirmation

[Jasmin Blanchette]

Hi all,

This is to confirm the rehearsals of my coming conference talks. As I  
wrote earlier, you probably want to choose one of two talks that you  
find more interesting. The TAP 2010 and ITP-10 talks share many of the  
same slides.


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.


IJCAR 2010
Monotonicity Inference for Higher-Order Logic
(joint work with Alex)
http://www4.in.tum.de/~blanchet/ijcar2010-mono.pdf
Wed. May 19, 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.


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.


I hope to see you there!

Regards,

Jasmin