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:FSL: A Program Logic for C11 Memory Fences
Speaker:Marko Doko
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:Friday, 16 October 2015
Time:13:00
Duration:60 Minutes
Location:Kaiserslautern
Building:G26
Room:111
Abstract
In this talk, we'll describe a simple, but powerful, program logic for reasoning
about C11 relaxed accesses used in conjunction with release and
acquire memory fences. Our logic, called fenced separation logic (FSL),
extends relaxed separation logic with special modalities for describing
state that has to be protected by memory fences. Like its precursor, FSL
allows ownership transfer over synchronizations and can be used to verify
the message-passing idiom and other similar programs. The soundness
of FSL has been established in Coq.
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/11/2016 11:00 AMLast modified by:Uwe Brahm/MPII/DE, 11/24/2016 04:13 PM
  • Maria-Louise Albrecht, 03/11/2016 11:02 AM -- Created document.