BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:d3ce4cc4-4d6e-4bf8-8223-5538abf3335c
X-WR-CALNAME:[MTV] Philipp Czerner (TUM) - Making IP = PSPACE Practical: Ef
 ficient Interactive Protocols for BDD Algorithms
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20251026T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20231029T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20241027T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20230326T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20240331T020000
RDATE:20250330T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:d3ce4cc4-4d6e-4bf8-8223-5538abf3335c
DTSTAMP:20260428T205213Z
CLASS:PUBLIC
DESCRIPTION:We show that interactive protocols between a prover and a verif
 ier\, a well-known tool of complexity theory\, can be used in practice to 
 certify the correctness of automated reasoning tools.\n\nTheoretically\, i
 nteractive protocols exist for all PSPACE problems. The verifier of a prot
 ocol checks the prover’s answer to a problem instance in probabilistic pol
 ynomial time\, with polynomially many bits of communication\, and with exp
 onentially small probability of error. (The prover may need exponential ti
 me.) Existing interactive protocols are not used in practice because their
  provers use naive algorithms\, inefficient even for small instances\, tha
 t are incompatible with practical implementations of automated reasoning.
 \n\nWe bridge the gap between theory and practice by means of an interacti
 ve protocol whose prover uses BDDs. We consider the problem of counting th
 e number of assignments to a QBF instance (#CP)\, which has a natural BDD-
 based algorithm. We give an interactive protocol for #CP whose prover is i
 mplemented on top of an extended BDD library. The prover has only a linear
  overhead in computation time over the natural algorithm.\n\nWe have imple
 mented our protocol in blic\, a certifying tool for #CP. Experiments on st
 andard QBF benchmarks show that blic is competitive with state-of-the-art 
 QBF-solvers. The run time of the verifier is negligible\, and the error pr
 obability is less than one millionth of a percent (and can easily be reduc
 ed further).
DTSTART;TZID=Europe/Paris:20240215T130000
DTEND;TZID=Europe/Paris:20240215T140000
LOCATION:salle 178\, zoom: https://bordeaux-inp-fr.zoom.us/j/89508306159
SEQUENCE:0
SUMMARY:[MTV] Philipp Czerner (TUM) - Making IP = PSPACE Practical: Efficie
 nt Interactive Protocols for BDD Algorithms
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
