BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verification of fine-grain concurrency: Separation Logic for Floyd
  assertions in Petri nets. - Tony Hoare\, Microsoft Research
DTSTART:20070117T141500Z
DTEND:20070117T151500Z
UID:TALK6213@talks.cam.ac.uk
CONTACT:Timothy G. Griffin
DESCRIPTION:The continuation of Moore's law will now depend on the skill o
 f\nprogrammers writing highly concurrent shared memory algorithms for\nmul
 ti-core architectures.  Correctness arguments are essential to avoid\nnon-
 deterministic errors\, including race conditions\, deadlocks and\nlivelock
 s.  These cannot be debugged\, but can readily be exploited by\nmalware.\n
 \nWe use pictorial representations of concurrent programs as Petri nets\;\
 nwe represent correctness by annotating the arcs with Floyd assertions.\nS
 eparation logic expresses the essential disjointness constraints for\nsafe
  and structured forms of concurrency.
LOCATION:Lecture Theatre 1\, Computer Laboratory
END:VEVENT
END:VCALENDAR