There are even more improvements (in some regard) to this, e.g. Affine Arithmetic[0, 1]. Here, error terms from different operations are accumulated symbolically so that in the case where they would cancel out (as could be useful for numerical algorithms), tighter bounds can be obtained.
There are several research groups working on improving such analyses.
--
[0] - https://en.wikipedia.org/wiki/Affine_arithmetic
[1] - http://users.ece.cmu.edu/~rutenbar/pdf/rutenbar-intervalicas...
edit: formatting