BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Explicit Stabilisation for Rely-Guarantee reasoning - John Wickers
 on (University of Cambridge)
DTSTART:20090605T130000Z
DTEND:20090605T140000Z
UID:TALK18272@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:Rely-guarantee (RG) is a compositional method that extends Hoa
 re-style reasoning to concurrent programs. A fundamental tenet is that any
  assertion we write must be _stable_\, that is\, invariant under any inter
 ference from concurrently-running threads. One can consider _stabilising_ 
 an assertion\, by weakening it (or strengthening it) until it becomes stab
 le. In this talk\, I will develop an extension to the RG method\, in which
  stabilisation is not a meta-level operator\, but exists within the syntax
  of assertions. I will show how this can eliminate many side-conditions fr
 om the RG proof rules\, and\, in particular\, lead to an elegant proof rul
 e for conditional statements whose tests are evaluated non-atomically. I w
 ill further show how explicit stabilisation might improve the modularity o
 f the RG method\, thus allowing the verification of libraries.\n\nThis tal
 k describes joint work with Matthew Parkinson.
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR