BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Local Reasoning about While-Loops - Thomas Tuerk (University of Ca
 mbridge)
DTSTART:20100525T120000Z
DTEND:20100525T130000Z
UID:TALK24361@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Separation logic is an extension of Hoare logic that allows lo
 cal reasoning. Local reasoning is a powerful feature that often allows sim
 pler specifications and proofs. However\, this power is not used to reason
  about while-loops.\n\nIn this talk an inference rule for the verification
  of the partial correctness of while-loops in Hoare logic is presented. In
  contrast to classical loop-invariants this inference uses pre- and post-c
 onditions for loops. It is not specific to separation logic. Instead\, it 
 represents a\nslightly different view on loops. It specifies what the loop
  will do instead of what has already been done. However\, the presented in
 ference gains its full potential by utilising the local reasoning provided
  by separation logic.\n\nThe inference rule has been implemented in the se
 paration logic tool Holfoot.\n\n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR