It’s astonishing how nobody hasn’t mentioned abstract interpretation yet. Under classical static analysis, if you can “prove” that a variable does not have values in some unsound zones, you can e.g. “prove” soundness or apply further optimizations.

The interval abstract domain works under interval analysis with an algebra that’s the same of this calculator. It’s funny to implement something like that on source/binary level :)