BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Playing in the Grey Area of Proofs - Laura Kovács\, Technical Uni
 versity of Vienna
DTSTART:20120919T100000Z
DTEND:20120919T110000Z
UID:TALK39946@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Interpolation is an important technique in verification and st
 atic analysis of programs. In particular\, interpolants extracted from pro
 ofs of various properties are used in invariant generation and bounded mod
 el checking. A number of recent papers studies interpolation in various th
 eories and also extraction of smaller interpolants from proofs. In particu
 lar\, there are several algorithms for extracting of interpolants from so-
 called local proofs.\n\nIn this talk we describe a technique of minimising
  interpolants based on transformations of what we call the "grey area" of 
 local proofs. We also present how to translate arbitrary proofs\, under ce
 rtain common conditions\, into local ones.\n\nUnlike many other interpolat
 ion techniques\, our technique is very general and applies to arbitrary th
 eories. Our approach is implemented in the theorem prover Vampire and eval
 uated on a large number of benchmarks coming from first-order theorem prov
 ing and bounded model checking using logic with equality\, uninterpreted f
 unctions and linear arithmetic. Our experiments demonstrate the power of t
 he new\ntechniques: for example\, it is not unusual that our proof transfo
 rmation gives more than a tenfold reduction in the size of interpolants.\n
 \nThis is a joint work with Krystof Hoder and Andrei Voronkov (The Univers
 ity of Manchester).
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR