Proving that programs cannot crash is important, especially in embedded programs that are critical. The abstract interpretation framework gives tools to prove such properties at scale. Expressing complex properties on program states (the possible values of variables at given program points) can be very costly. This is why symbolic methods have been developed: to keep relationships between variables by reasoning directly over the arithmetic expressions, and to apply sound program transformations on the fly to facilitate analysis. In many popular programming languages that manipulate fixed-length integer variables, overflows and casts act as modulos that hinder the use of regular symbolic methods. We present an abstract domain that safely rewrites arithmetic expressions into simpler ones. In particular, modulo computations are safely discarded: either by proving that they can be accurately described, or by replacing them conservatively. We can also take advantage of the simplified form of arithmetic expressions to match patterns and simplify them. We illustrate this method with the detection of linear interpolations.
