Campus Event Calendar
Event Entry
What and Who
Compositional Verification of Termination-Preserving Refinement of Concurrent Programs
Hongjin Liang
UST China
SWS Colloquium
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.
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 23 July 2014
10:30
90 Minutes
G26
113
Kaiserslautern
Abstract
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.
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.
Contact
Viktor Vafeiadis
--email hidden
Video Broadcast
Yes
Saarbrücken
E1 5
029
passcode not visible
logged in users only
Susanne Girard, 07/16/2014 12:38 -- Created document.