Problems of existing simulations Considers no env. in CompCert (Leroy et al J O NOT compositional w.r.t. parallel composition Assumes arbitrary env. in process calculus (e.g. (Milner et al. a Too strong: limited applications Our rsim Parameterized with the interference with eny e Compositional e More applications Use rely/guarantee to specify the interferenceProblems of existing simulations : Our RGSim: • Considers no env. in CompCert[Leroy et al.]  NOT compositional w.r.t. parallel composition • Assumes arbitrary env. in process calculus (e.g. [Milner et al.])  Too strong: limited applications • Parameterized with the interference with env. ☺ Compositional ☺ More applications • Use rely/guarantee to specify the interference