BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Microsoft Research Cambridge\, public talks
SUMMARY:Playing in the Grey Area of Proofs - Laura KovĂˇcs\
, Technical University of Vienna
DTSTART;TZID=Europe/London:20120919T110000
DTEND;TZID=Europe/London:20120919T120000
UID:TALK39946AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/39946
DESCRIPTION:Interpolation is an important technique in verific
ation and static analysis of programs. In particul
ar\, interpolants extracted from proofs of various
properties are used in invariant generation and b
ounded model checking. A number of recent papers s
tudies interpolation in various theories and also
extraction of smaller interpolants from proofs. In
particular\, there are several algorithms for ext
racting of interpolants from so-called local proof
s.\n\nIn this talk we describe a technique of mini
mising interpolants based on transformations of wh
at we call the "grey area" of local proofs. We als
o present how to translate arbitrary proofs\, unde
r certain common conditions\, into local ones.\n\n
Unlike many other interpolation techniques\, our t
echnique is very general and applies to arbitrary
theories. Our approach is implemented in the theor
em prover Vampire and evaluated on a large number
of benchmarks coming from first-order theorem prov
ing and bounded model checking using logic with eq
uality\, uninterpreted functions and linear arithm
etic. Our experiments demonstrate the power of the
new\ntechniques: for example\, it is not unusual
that our proof transformation gives more than a te
nfold reduction in the size of interpolants.\n\nTh
is is a joint work with Krystof Hoder and Andrei V
oronkov (The University of Manchester).
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7
J J Thomson Avenue (Off Madingley Road)\, Cambrid
ge
CONTACT:Microsoft Research Cambridge Talks Admins
END:VEVENT
END:VCALENDAR