![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Computer Laboratory Wednesday Seminars > Verification of fine-grain concurrency: Separation Logic for Floyd assertions in Petri nets.
![]() Verification of fine-grain concurrency: Separation Logic for Floyd assertions in Petri nets.Add to your list(s) Download to your calendar using vCal
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:
Note that ex-directory lists are not shown. |
Other listsThe obesity epidemic: Discussing the global health crisis Continuity in Education and Cultural links between countries: Brexit Talk and Q&A Computer Laboratory Security SeminarOther talksSouth American Opuntioids Exhibiting Ice Age Cambridge Debtors’ schedules: a new source for understanding the economy in 18th-century England Climate change, archaeology and tradition in an Alaskan Yup'ik Village NatHistFest: the 99th Conversazione and exhibition on the wonders of the natural world. Project Management |