What is PILAT ?

PILAT (for Polynomial Invariants by Linear Algebra Tool) is an invariant generator based on the study of matrices. It processes loops with polynomial assignments and linearize them, then searches for left eigenvectors of the resulting matrix. Those vectors expresses invariants of the loop.

Pilat is a plug-in of the Frama-C framework. It is written in Ocaml and it is open source under LGPL licence, you can find it here. If you use OPAM, you can get the latest version with "opam install pilat". We applied our tool to this benchmark on deterministic loops and on non-deterministic loops.