Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
Speaker:Ralf Jung
coming from:Max Planck Institute for Software Systems
Speakers Bio:
Event Type:SWS Student Defense Talks - Qualifying Exam
We use this to send out email in the morning.
Level:Expert Audience
Date, Time and Location
Date:Tuesday, 18 August 2015
Duration:60 Minutes
Building:E1 5
We present Iris, a concurrent separation logic with a simple premise:
Monoids and invariants are all you need. Partial commutative monoids
enable us to express—and invariants enable us to enforce—user-defined protocols

on shared state, which are at the conceptual core of most
recent program logics for concurrency. Furthermore, through a novel
extension of the concept of a view shift, Iris supports the encoding
of logically atomic specifications, i.e., Hoare-style specs that
permit the client of an operation to treat the operation essentially
as if it were atomic, even if it is not.

Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Maria-Louise Albrecht, 03/14/2016 10:36 AM -- Created document.