[Club2] Tue, Aug. 16 and Wed, Aug. 17 - talks by Nick Smallbone and Sascha Boehme

[Andrei Popescu]

Dear all,

Next week we have 3 talks, on Tuesday and Wednesday, by our visitor Nick Smallbone and by Sascha. Details below. 

Andrei  

FIRST TALK, by Nick Smallbone:  

QuickSpec: Guessing Formal Specifications using Testing
====================================================
Tue. Aug 16, 14:00, MI 00.09.055 ("Alan Turing")

(please note that this first talk is on Tuesday, not Wednesday, our regular Club2 talk day)

QuickSpec is a tool that automatically generates algebraic specifications for sets of pure functions. The tool is based on testing, rather than static analysis or theorem proving. The main challenge QuickSpec faces is to keep the number of generated equations to a minimum while maintaining completeness.


SECOND TALK, by Nick Smallbone:  
 
Monotonox: From Typed to Untyped First-Order Logic, Efficiently
====================================================
Wed. Aug 17, 14:00, MI 00.09.055 ("Alan Turing")

Many interesting problems are more naturally expressed in many-sorted
first-order logic than in unsorted logic, but most existing highly-efficient automated theorem provers solve problems only in unsorted logic. Conversely, some reasoning tools, for example model finders, can make good use of sort-information in a problem, but most problems today are formulated in unsorted logic. I present a novel analysis for sorted logic, which determines if a given sort is monotone. The domain of a monotone sort can always be extended with an extra element. This analysis significantly improves well-known translations between unsorted and many-sorted logic.


THIRD TALK, by Sascha Boehme: 
 
Glancing behind the Scenes: Satisfiability Modulo Theories
====================================================
Wed. Aug 17, 15:00, MI 00.09.055 ("Alan Turing")

 Satisfiability Modulo Theories (SMT) solvers have been found
 useful within the context of Isabelle, but besides their names
 (for instance "Z3") little seems to be known about them.  In
 this talk, I try to give some insights into the "little engines
 of proof" that are hidden in an off-the-shelf SMT solver: SAT
 solvers, equality reasoning, instantiation of quantifiers, and
 some of the supported theories.  I intend to give an overview
 without going too much into (implementation) details.  There
 should be plenty of time for questions.