Steven de Oliveira

Ph.D. Student in formal methods


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.


Related publications

  1. De Oliveira Steven, Bensalem Saddek and Prevosto Virgile(2017, October)
    Synthesizing invariants by solving solvable loops
  2. De Oliveira Steven, Bensalem Saddek and Prevosto Virgile (2016, October)
    Polynomial invariants by linear algebra
  3. De Oliveira Steven, Bensalem Saddek and Prevosto Virgile (2016, June)
    Alg├Ębre lineaire pour invariant polynomiaux (slides)