University of Cambridge > Talks.cam > Wednesday Seminars - Department of Computer Science and Technology  > Verification of fine-grain concurrency: Separation Logic for Floyd assertions in Petri nets.

  Browse A-Z

Log in

Cambridge users (raven)details Other usersdetails No account?details

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

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 Wednesday Seminars - Department of Computer Science and Technology series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

The obesity epidemic: Discussing the global health crisis Continuity in Education and Cultural links between countries: Brexit Talk and Q&A Computer Laboratory Security Seminar

Other talks

EU LIFE Lecture - "Histone Chaperones Maintain Cell Fates and Antagonize Reprogramming in C. elegans and Human Cells" NatHistFest: the 99th Conversazione and exhibition on the wonders of the natural world. Climate change, archaeology and tradition in an Alaskan Yup'ik Village Debtors’ schedules: a new source for understanding the economy in 18th-century England Exhibiting Ice Age Cambridge South American Opuntioids The Gopakumar-Vafa conjecture for symplectic manifolds The role of myosin VI in connexin 43 gap junction accretion Throwing light on organocatalysis: new opportunities in enantioselective synthesis Cambridge-Lausanne Workshop 2018 - Day 2 A feast of languages: multilingualism in neuro-typical and atypical populations Project Management
 

© 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity