Simulation in Comp Cert Leroy et al e Can verify refinement of sequential programs O NOT compositional w.r.t. parallel composition O Consider no environments Simulation in process calculus(e . ccs (Milner et.) Assume arbitrary environments Compositional Too strong: limited applicationsSimulation in CompCert [Leroy et al.] ☺ Can verify refinement of sequential programs  NOT compositional w.r.t. parallel composition  Consider NO environments Simulation in process calculus(e.g. CCS [Milner et al.]) • Assume arbitrary environments ☺ Compositional  Too strong: limited applications