Status Updates From Introduction to Static Anal...

Widening: suppose I have a state A that transitions via a step S to A', and then S repeats indefinitely. Determining U A{'...} is evidently impossible. So instead, what we do over-approximate A U A' by (1) keeping the constraints common to both A and A' and (2) throwing out the constraints of A that are no longer valid constraints on A'. This is clearly monotonically decreasing in # of constraints and will converge.