[Club2] ITP dry run

[Sascha Boehme]

Hi all,

on Thursday (24 June) at 15:00, I will do a rehearsal of my ITP talk,
in Turing (00.09.055).  See below for an abstract.

Sascha


Fast LCF-Style Proof Reconstruction for Z3

The Satisfiability Modulo Theories (SMT) solver Z3 can generate proofs
of unsatisfiability.  We present independent reconstruction of these
proofs in the theorem provers Isabelle/HOL and HOL4 with particular
focus on efficiency.  Our highly optimized implementations outperform
previous LCF-style proof checkers for SMT, often by orders of
magnitude.  Detailed performance data shows that LCF-style proof
reconstruction can be faster than proof search in Z3.