Inference of polynomial invariants for imperative programs: A farewell to Grbner 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 Grbner bases.
polynomial invariants static analysis abstract interpretation