[Club2] Talk by Tjark Weber on July 2

[Jasmin Christian Blanchette]

Dear all,

Tjark Weber will visit us on July 2 and give a talk titled

    Validating QBF Invalidity in HOL4

(see abstract below). It will take place at 11:00 in room 00.09.055 (Alan Turing) in Garching.

I hope to see you there!

Jasmin


Abstract:

The Quantified Boolean Formulae (QBF) solver Squolem can generate certificates of invalidity, based on Q-resolution. I present independent checking of these certificates in the HOL4 theorem prover. This enables HOL4 users to benefit from Squolem's automation for QBF problems, and provides high correctness assurances for Squolem's results. Detailed performance data shows that LCF-style certificate checking is feasible even for large QBF instances. The work prompted improvements to HOL4's inference kernel.

Bio:

Tjark Weber obtained his Ph.D. from TU München in 2008 for work on finite model generation and an integration of SAT solvers with the interactive theorem prover Isabelle/HOL.  He is now integrating SMT solvers with interactive theorem provers at the University of Cambridge.