package why3

  1. Overview
  2. No Docs
Next generation of the Why software verification platform

Install

Dune Dependency

Authors

Maintainers

Sources

why3-0.80.tar.gz
md5=4b50adf812a34879be92f27f25be7ec9

Description

Why3 clearly separates the purely logical specification part from generation of verification conditions for programs. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants.

Published: 21 Nov 2013

Dependencies (5)

  1. sqlite3
  2. alt-ergo
  3. coq = "8.3"
  4. ocamlgraph = "1.8.2"
  5. ocaml < "4.06.0"

Dev Dependencies

None

Used by

None

Conflicts

None