Outline Rely-Guarantee-based simulation for modular verification of concurrent refinement Logic for linearizability Progress properties and contextual refinementOutline • Rely-Guarantee-based simulation for modular verification of concurrent refinement • Logic for linearizability • Progress properties and contextual refinement