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 -pilat-degree n.