[Club2] Talks by Krystof Hoder this Tuesday and Wednesday from 3:30 in the Turing room

[Andrei Popescu]

Dear All,  
The coming week, we have two talks from Krystof Hoder: on Tuesday, a general description of the Vampire theorem prover, and on Wednesday a more technical talk on interpolation and fixed points applied to
 verification.  Details below.  
Best regards,   Andrei 

First talk: Krystof Hoder The Vampire Theorem Prover====================================================Tue. Feb. 7, 15:30, MI 00.09.055 ("Alan Turing")
Vampire ( http://vprover.org ) is one of the best performing first-order theorem provers, consistently winning several divisions of the CASC theorem prover championship for the past ten years. This talk will give a basic overview of its internals, such as the resolution and superposition calculus, preprocessing, indexing structures and splitting. A particular attention will be given to the Sine axiom selection algorithm which helps with reasoning on problems with large amounts of axioms.

Second talk: Krystof Hoder Interpolants, Fixed-Points and Verification====================================================Wed. Feb. 8, 15:30, MI 00.09.055 ("Alan
 Turing")
The talk will consist of two parts. The first will give a brief introduction on interpolation and present a technique for interpolant generation based on local proofs. We will also talk about some recent extensions of this method, such as interpolant minimization which uses pseudo-boolean optimization to generate
 better interpolants.In the second part we will present μZ, a tool built on the top of the Z3 SMT solver, with Datalog-like interface, support for theories and abstract interpretations, and with a portfolio of solving strategies. We will briefly mention our recent work on a property directed reachability algorithm for model checking.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20120204/f2b261bb/attachment.html>