Michael Petter and Helmut Seidl. Inferring Polynomial Invariants. Workshop on Numerical and Symbolic Abstract Domains, Paris, France, 2005.
Polyinvar is a tool to infer valid polynomial relations at program points in the control flow graph of Java Code. This analysis is achieved by an incremental fixpoint iteration over a set of polynomial modules, representing the weakest precondition for a generic relation of degree n at a given program point.