Integrating SAT, QBF and SMT Solvers with Interactive Theorem Provers
Workshop on Trusted Extensions of Interactive Theorem Provers; Cambridge, UK; August 11, 2010
»
More presentations by Tjark Weber
Independent Proof Reconstruction for Z3: An Overview
Tjark Weber on
Z3 Special Interest Group Meeting; Microsoft Research Cambridge; 3 November, 2011
Integrating SAT, QBF and SMT Solvers with Interactive Theorem Provers
Tjark Weber on
Foundations of Software Systems, University of Sussex (UK); January 12, 2011
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL
Tjark Weber on
CPP 2011; Kenting, Taiwan; 8 December, 2011