BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/313
DTSTAMP:20230914T125919Z
SUMMARY:Proof Transformations for Verification
DESCRIPTION:Speaker: Ashutosh K. Gupta (Institute of Science and Technology
\, Austria\nAm Campus 1\n3400 Klosterneuburg\nAustria)\n\nAbstract: \nVari
ous verification methods depend on theorem provers to obtain proofs of ver
ification conditions. If the provers return proofs that satisfy certain st
ructure then it may enhance the performance of the verification methods. T
heorem provers aim to find the proofs using the most efficient algorithms.
Therefore\, the returned proofs from the existing theorem provers may not
satisfy such structures. In my talk\, I will present two pieces of our wo
rk that transform the proofs produced by the provers to obtain such struct
ured proofs.\n\nIn the first work\, we present a new efficient parametrize
d method to remove redundant parts of resolution proofs. The parameter all
ows one to choose between coverage of the redundancy removal and the effic
iency of the method.\n\nIn the second work\, we present a set of proof tra
nsformation rules that obtains "localize proofs" from proofs of unsatisfia
ble formulas. The localize proofs allow one to compute (tree)-interpolants
efficiently.\n
URL:https://www.tcs.tifr.res.in/web/events/313
DTSTART;TZID=Asia/Kolkata:20121012T153000
DTEND;TZID=Asia/Kolkata:20121012T163000
LOCATION:A-212 (STCS Seminar Room)
END:VEVENT
END:VCALENDAR