Our Contributions(Part 1) RGSim Rely/Guarantee Simulation Compositional w.r.t. parallel composition Flexible applicable optimizations in concurrent contexts concurrent gc fine-grained concurrent objOur Contributions (Part 1) • RGSim = Rely/Guarantee + Simulation – Compositional w.r.t. parallel composition – Flexible & applicable • optimizations in concurrent contexts • concurrent GC • fine-grained concurrent obj. • …