10Non-termination conditions could also be propagated backwards to provide an over-approximation of the conditions under which an application never terminates, i.e. conditions for liveness.