package pilat
A Frama-C polynomial invariant generator
Install
Dune Dependency
Authors
Maintainers
Sources
stable_1.1.zip
sha256=6843cd0783d7060494ab5d19d4c135b53e1ca1bfd27ad385ecd73c827188e830
md5=aa4f9778e377a1931b46920e68ab7b1c
Description
This tool generates invariants of linear and polynomial loops, with deterministic and non deterministic assignments, as annotations in the initial source code.
Published: 09 Nov 2017
On This Page