dW differential weakening tries proving the postcondition P of a differential equation system [{x'=f(x) & Q}]P from its evolution domain constraint Q by reducing it to Q→P. If this succeeds, the property is independent of x′=f(x).

See also

Learning resources