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.
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.