BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:On Scalable Shape Analysis - Hongseok Yang (Queen Mary\, Universit
 y of London)
DTSTART:20080118T140000Z
DTEND:20080118T150000Z
UID:TALK9335@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:Shape analysis is a precise form of pointer analysis\, which\n
 can be used to verify deep properties of data structures such as whether\n
 or not they are cyclic\,whether they are nested\, etc. Shape analyses are\
 nalso expensive\, and the tremendous number of abstract states they genera
 te is an impediment to\ntheir use in verification of sizeable programs. In
  this talk\, I will describe the techniques\nfor improving the scalability
  of shape analyses. With these techniques\, we have improved\nour analysis
  that was able to handle programs of up to 1\,000 lines\, such that it can
  now analyze\nprograms of up to 10\,000 lines. Our experiments also show t
 hat the new analysis\nis precise. It identifies memory safety errors and m
 emory leaks\nin several Windows and Linux device drivers and\, after\nthes
 e bugs are fixed\, it automatically proves integrity of pointer manipulati
 on for\nthese drivers.\n\nThis order of magnitude improvement in sizes of 
 programs verified is obtained by\ncombining several ideas. One is the loca
 l reasoning idea of separation logic\, which\nreduces recomputation of ana
 lysis of procedure bodies\, and which allows\nefficient transfer functions
  for primitive program statements.\nAnother is an interprocedural analysis
  algorithm which aggressively discards intermediate\nstates. The most impo
 rtant new technical contribution of the work is a new\njoin (or widening) 
 operator\, which greatly reduces the number of abstract states\nused by th
 e analysis while not greatly reducing precision\; the join is also\nintegr
 ated with procedure summaries in an interprocedural analysis.\n\nThis is j
 oint work with Oukseh Lee\, Cristiano Calcagno\, Dino Distefano and Peter 
 O'Hearn.\n\n
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR