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
sha256=717409946dc83f020f3c0b453758261e33fab97bd4544c757620ba48d8ba2730
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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct