package pilat

  1. Overview
  2. No Docs
A Frama-C polynomial invariant generator

Install

Dune Dependency

github.com Edit opam file Versions (4)

Authors

  1. S
    Steven De Oliveira <de.oliveira.steven@gmail.com>

Maintainers

  1. S
    Steven De Oliveira <de.oliveira.steven@gmail.com>

Sources

stable_1.2.zip
md5=e14eae3df08778154824564c8a98eadf

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 Jun 2018

Dependencies (5)

  1. frama-c >= "17.0" & < "20.0"
  2. zarith < "1.8"
  3. lacaml
  4. ocamlfind build
  5. ocaml > "4.02.3"

Dev Dependencies

None

Used by

None

Conflicts

None