package why3
- Overview
- No Docs
You can search for identifiers within the package.
in-package search v0.2.0
Next generation of the Why software verification platform
Install
Dune Dependency
Authors
Maintainers
Sources
why3-0.80.tar.gz
sha256=32efd5d95744e7e67d223232a2cb6473d126b50d86c3a18f5971f04df08e6f9b
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)
- sqlite3
- alt-ergo
-
coq
= "8.3"
-
ocamlgraph
= "1.8.2"
-
ocaml
< "4.06.0"
Dev Dependencies
None
Used by
None
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page