Pilat, the Polynomial Invariant through Linear Algebra Tool, is a plug-in for generating (polynomial) numerical invariants over the loops of the program. Note that it is currently restricted to arithmetic variables.
Pilat is available as an external open-source plug-in. Once installed, it is enabled with the
-pilat option, which will try to generate all polynomial invariants that may exist in the loops of the program.
Pilat finds all invariants that exist up to a certain degree. By default, this degree is 2, but this can modified with