Copenhagen Programming Language Seminar
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 email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org