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.73.tar.gz
sha256=99653cd09a90776b975393ca14bdfc1fb3402b7a98ff40930d4fe3a57e6ce368
md5=8994f147b7fc4084da46e81693e044bb
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