Symbolic transformation of expressions in modular arithmetic
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…