Verification of fine-grain concurrency: Separation Logic for Floyd assertions in Petri nets.

Add to your list(s) Download to your calendar using vCal

• Tony Hoare, Microsoft Research
• Wednesday 17 January 2007, 14:15-15:15
• Lecture Theatre 1, Computer Laboratory.

If you have a question about this talk, please contact Timothy G. Griffin.

The continuation of Moore’s law will now depend on the skill of programmers writing highly concurrent shared memory algorithms for multi-core architectures. Correctness arguments are essential to avoid non-deterministic errors, including race conditions, deadlocks and livelocks. These cannot be debugged, but can readily be exploited by malware.

We use pictorial representations of concurrent programs as Petri nets; we represent correctness by annotating the arcs with Floyd assertions. Separation logic expresses the essential disjointness constraints for safe and structured forms of concurrency.

This talk is part of the Computer Laboratory Wednesday Seminars series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Chris Davis' list
• Computer Laboratory Wednesday Seminars
• Computer Laboratory talks
• Graduate-Seminars
• Guy Emerson's list
• Interested Talks
• Lecture Theatre 1, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• computer science
• se393's list

Note that ex-directory lists are not shown.