BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verifying malloc using RGSep and 'Explicit Stabilisation' - John W
 ickerson (University of Cambridge)
DTSTART:20091026T124500Z
DTEND:20091026T140000Z
UID:TALK20698@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:The talk will introduce a new formalisation of stability for R
 ely-Guarantee\,\nin which an assertion's stability is encoded into its syn
 tactic form. I'll\nbriefly show how this allows library code to be specifi
 ed independently\nof its various calling environments. But the main thrust
  of the talk concerns\nhow this so-called 'explicit stabilisation' can be 
 applied to RGSep\, a recent\naddition to the Rely-Guarantee family. Doing 
 so enables an 'InfoHiding'\nrule\, which describes how a (sequential) modu
 le can hide its 'internal interference'\nfrom clients. We illustrate with 
 a proof of the memory management module\nfrom Version 7 Unix.\n
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR