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:Compositional Verification of Termination-Preserving Refinement of Concurrent Programs
Speaker:Hongjin Liang
coming from:UST China
Speakers Bio:Hongjin and her advisor have been been working on program logics for
proving refinement of concurrent programs and have been publishing at
top places: POPL, PLDI, LICS, CONCUR.
Event Type:SWS Colloquium
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Date, Time and Location
Date:Wednesday, 23 July 2014
Duration:90 Minutes
Many verification problems can be reduced to refinement verification.
However, existing work on verifying refinement of concurrent
programs either fails to prove the preservation of termination, allowing
a diverging program to trivially refine any programs, or is
difficult to apply in compositional thread-local reasoning. In this
talk, I will present a Hoare-style concurrent program logic
supporting termination-preserving refinement proofs. We show two
key applications of our logic, i.e., verifying linearizability and
lock-freedom together for fine-grained concurrent objects, and verifying
full correctness of optimizations of concurrent algorithms.
Name(s):Viktor Vafeiadis
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Saarbr├╝cken
To Building:E1 5To Room:029
Meeting ID:
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Susanne Girard, 07/16/2014 12:38 PM -- Created document.