Polynomial Analysis of Modular Arithmetic.

The modular polynomial abstract domain, MPAD, is proposed, whose invariants are systems of polynomial equations that hold modulo a power of 2. Its domain operations are founded on a closure operation, but unlike conventional polynomial abstractions, MPAD satisfies the ascending chain condition, can model both positive and negative polynomial guards, and can infer invariants previously out of reach.