Invariant-Based Verification 90 C1 C2 S2 C3 6 Initial condition:Inv(So) Progress: if Inv(s),then 3s'.ss. Preservation: if Inv(s)and s s',then Inv (S').Invariant-Based Verification Initial condition: Inv(S0) S0 c1 S1 c2 S2 c3 … cn Sn Progress: if Inv(S), then S’. S c S’. Preservation: if Inv(S) and S c S’, then Inv(S’)