BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Towards Automatic Stability Analysis for Rely-Guarantee Proofs - H
 asan Amjad (Middlesex University)
DTSTART:20081028T130000Z
DTEND:20081028T140000Z
UID:TALK13422@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:The Rely-Guarantee approach is a well-known compositional meth
 od for proving Hoare logic properties of concurrent programs. In this appr
 oach\, predicates in the proof must be proved invariant (or stable) under 
 interference from the environment. I'll talk about progress towards a meth
 od for automatically detecting and repairing instability in such proofs (a
 nd all the concomitant limitations of such automation). The method uses a 
 combination of model checking\, abstract interpretation\,\nSMT and flow-co
 ntrol refinement. This is joint work with Richard Bornat.\n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR