BEGIN:VCALENDAR
PRODID:-//eluceo/ical//2.0/EN
VERSION:2.0
CALSCALE:GREGORIAN
BEGIN:VEVENT
UID:www.tcs.tifr.res.in/event/331
DTSTAMP:20230914T125920Z
SUMMARY:Program Analysis Using Quantifier Elimination Heuristics
DESCRIPTION:Speaker: Deepak Kapur (The University of New Mexico\nDepartment
  of Computer Science\nAlbuquerque\, NM 87131\nUnited States of America)\n\
 nAbstract: \nLoop invariants play a central role in ensuring the reliabili
 ty of software. Program analysis techniques must either require such progr
 am annotations at appropriate program locations or automatically derive th
 ese annotations from a program.  A new approach for automatically generat
 ing loop invariants from imperative programs will be presented.  Loop inv
 ariants are assumed to have certain shape\, i.e.\, they are formulas in a 
 restricted quantifier-free first-order theory. Elimination techniques can 
 be used to generate such invariants.  The focus of this talk will be on e
 xploring heuristics for quantifier-elimination so that such techniques can
  scale well.  A nice feature of the proposed approach is that it does not
  need to have access to any specification or annotations associated with a
  program. Some preliminary ideas about how to generalize these approaches 
 to work on data types other than numbers will be discussed.\n
URL:https://www.tcs.tifr.res.in/web/events/331
DTSTART;TZID=Asia/Kolkata:20130108T110000
DTEND;TZID=Asia/Kolkata:20130108T120000
LOCATION:AG-80
END:VEVENT
END:VCALENDAR