BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Locality and Footprints in Separation Logic - Mohammad Raza (Imper
 ial College)
DTSTART:20091019T114500Z
DTEND:20091019T130000Z
UID:TALK20697@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:Local reasoning based on separation logic captures the natural
  local\nbehaviour of programs by allowing reasoning to focus on the footpr
 ints\nof commands. In the semantic formalization of abstract separation\nl
 ogic\, programs are modelled as "local functions" that act locally on\nabs
 tract resource models. However\, certain issues related to dynamic\nalloca
 tion force some non-intuitive choices in the general definition\nof locali
 ty\, and lead to some unnatural outcomes. For example\, the\nsafety footpr
 ints of a program do not always yield a complete\nspecification of the pro
 gram\, and one is forced to work with\nnon-deterministic allocation in unb
 ounded memory. We investigate these\nissues\, and first present a formaliz
 ation of "completeness footprints"\nwhich yield complete specifications. W
 e then present an alternative\nmemory model in which completeness footprin
 ts do correspond to safety\nfootprints\, and deterministic or bounded memo
 ry allocation can be\nmodelled as local functions. More generally\, a stro
 nger notion of\nlocality is identified which provides the correspondence b
 etween\nsafety and completeness footprints for arbitrary resource models.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR