Outline Rely-Guarantee-based simulation for modular verification of concurrent refinement Logic for linearizability Progress properties and contextual refinement
Outline • Rely-Guarantee-based simulation for modular verification of concurrent refinement • Logic for linearizability • Progress properties and contextual refinement
Modular verification of tcs T1 S1 T2 S2 (Compositionality) T1 T2 9 S1 $2
(Compositionality) T1 || T2 S1 || S2 T1 S1 T2 S2 Modular Verification of T S