Simulation in Comp Cert Leroy et al e Can verify refinement of sequential programs O NOT compositional w.r.t. parallel composition S local ti x++; 七=x print(x)i t+1 print(x )i We have t<s but not t‖Tss|sT: local t; t = x; x = t + 1; print( x ); S: x++; print( x ); We have T  S , but not T||T  S||S Simulation in CompCert [Leroy et al.] ☺ Can verify refinement of sequential programs  NOT compositional w.r.t. parallel composition