Copenhagen Programming Language Seminar

RGsep: separation logic for fine-grained concurrency

Viktor Vafeiadis
Microsoft Research Cambridge

Tuesday October 20, 15:00 - 16:00
The IT University, Rued Langgaards Vej 7, DK-2300,  Auditorium 4


In order to reason about fine-grain concurrent programs, Matthew Parkinson and I introduced RGSep, a program logic that incorporates rely-guarantee reasoning into separation logic. I shall give a brief overview of this logic, and describe a recent automatic verification procedure based on it.

Action inference takes a program and computes a set of RGSep actions, which overapproximate the interference that each thread causes to its concurrent environment. We have used action inference to verify safety, liveness, and functional correctness properties of a number of practical concurrent algorithms.

Host: Lars Birkedal

Scientific host:Lars Birkedal Administrative host:Renée Korver Michan. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org