package pilat

  1. Overview
  2. No Docs
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

Dependencies (5)

  1. frama-c
  2. zarith < "1.8"
  3. lacaml
  4. ocamlfind
  5. ocaml > "4.02.3"

Dev Dependencies

None

Used by

None

Conflicts (1)

  1. frama-c >= "17.0"
OCaml

Innovation. Community. Security.