Verifying Invariants of Lock-free Data Structures with Rely-Guarantee and Refinement Types
ACM Transactions on Programming Languages and Systems (TOPLAS), 39(3) 2017
2016 Impact Factor (JCR): 3.033.