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.1.zip
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"