pilat

AuthorSteven De Oliveira <de.oliveira.steven@gmail.com>
LicenseLGPLv2.1
Homepagehttps://github.com/Stevendeo/Pilat/
Issue Trackerhttps://github.com/Stevendeo/Pilat/issues
MaintainerSteven De Oliveira <de.oliveira.steven@gmail.com>
Dependencies
&frama-c>= 20180501
lacaml
ocamlfind
zarith
Availableocaml-version > "4.02.3"
PublishedJun 6, 2018
Source [http] https://github.com/Stevendeo/Pilat/archive/stable_1.2.zip
e14eae3df08778154824564c8a98eadf
StatisticsNot installed in the last month.
Edithttps://github.com/ocaml/opam-repository/tree/master/packages/pilat/pilat.1.2/opam

A Frama-C polynomial invariant generator

This tool generates invariants of linear and polynomial loops, with deterministic and non deterministic assignments, as annotations in the initial source code.

No package is dependent