BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Validating QBF Validity in HOL4 - Tjark Weber (University of Cambr
 idge)
DTSTART:20110315T131500Z
DTEND:20110315T141500Z
UID:TALK29336@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:The Quantified Boolean Formulae (QBF) solver Squolem can gener
 ate\ncertificates of validity\, based on Skolem functions.  We present\nin
 dependent checking of these certificates in the HOL4 theorem prover.\nThis
  enables HOL4 users to benefit from Squolem's automation for\nvalid QBF pr
 oblems.  Detailed performance data shows that LCF-style\nchecking of valid
 ity certificates is often (but not always) feasible\neven for large QBF in
 stances.  Additionally\, our work provides high\ncorrectness assurances fo
 r Squolem's claims of validity and uncovered\na soundness bug in a previou
 s version of its certificate validator\nQBV.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR