Max-Planck-Institut für Informatik
max planck institut
informatik
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
Visibility:SWS
We use this to send out email in the morning.
Level:Expert Audience
Language:English
Date, Time and Location
Date:Tuesday, 18 August 2015
Time:13:00
Duration:60 Minutes
Location:Saarbrücken
Building:E1 5
Room:029
Abstract
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.

Contact
Name(s):
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):

Created by:Maria-Louise Albrecht/MPI-KLSB, 03/14/2016 10:32 AMLast modified by:Uwe Brahm/MPII/DE, 11/24/2016 04:13 PM
  • Maria-Louise Albrecht, 03/14/2016 10:36 AM -- Created document.