BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Modular verification of concurrent programs with heap - Alexey Got
 sman (ARG)
DTSTART:20090303T130000Z
DTEND:20090303T140000Z
UID:TALK17307@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Reasoning about concurrent programs is made difficult by the n
 umber of possible interactions between threads. This is especially true fo
 r heap-manipulating programs\, in which threads can interact in subtle way
 s via\ndynamically-allocated data structures. I will present novel thread-
 modular logics and analyses for concurrent heap-manipulating programs that
  address this challenge. The logics and the analyses can be used to reason
  about or automatically verify a number of safety properties (memory safet
 y\, data race freedom\, absence of memory leaks) and have been successfull
 y used as a key\ningredient in methods for verifying liveness properties. 
 I will also discuss my approach to their design in which program logics an
 d program analyses share the underlying reasoning principles.\n\nThis is a
  rehearsal of my job talk. The talk does not contain any new results: all 
 the results have already been presented at previous ARG Lunches.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR