Verifying Invariants of Lock-free Data Structures with Rely-Guarantee and Refinement Types
ACM Transactions on Programming Languages and Systems (TOPLAS), 39(3) 2017