BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Bound Analysis of Imperative Programs with the Size-change Abstrac
 tion - Florian Zuleger\, TU Wien
DTSTART:20111201T140000Z
DTEND:20111201T150000Z
UID:TALK34601@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:The size-change abstraction (SCA) is an important program abst
 raction for termination analysis\, which has been successfully implemented
  in many tools for functional and logic programs. In this talk\, I will de
 monstrate that SCA is also a highly effective abstract domain for the boun
 d analysis of imperative programs. I will introduce the first algorithm fo
 r bound computation with SCA and discuss how our methodology solves the te
 chnical challenges involved in bound computation. Further I will present t
 wo program transformations - pathwise analysis and contextualization - tha
 t make our SCA-based analysis precise enough to scale to real world progra
 ms. I will demonstrate the effectiveness of our approach by experiments wi
 th our tool Loopus on the cBench benchmark.
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR