Inference of polynomial invariants for imperative programs: A farewell to Gröbner bases

• A static analysis for computing polynomial invariants of imperative programs.
• The algorithm can find a large majority of loop invariants reported in previous work.
• Its implementation is significantly faster than implementations using Gröbner bases.

The article presents a static analysis for computing polynomial invariants for imperative programs. The analysis is derived from an abstract interpretation of a backwards semantics, and computes preconditions for equalities of the form g=0g=0 to hold at the end of execution. A distinguishing feature of the technique is that it computes polynomial loop invariants without resorting to Gröbner base computations. The analysis uses remainder computations over parameterized polynomials in order to handle conditionals and loops efficiently. The algorithm can analyze and find a large majority of loop invariants reported previously in the literature, and executes significantly faster than implementations using Gröbner bases.