package alt-ergo-plugin-ab-why3
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=39e2c9128a7d1e89f332e31a2716f359f3b9e1a925fe81f11fa4a749b5d24d82
sha512=ca953fe5a4964287de7e328ec4e3724a9baaa908c22862b075da5870bbf3707c7f78bd9fe0af98ee6c6382b5de0a4ddfcc93e09dc8b5b8e7d6ab6b1196a0656d
Description
An experimental front-end that parses a subset of Why3's logic. More precisely, this front-end targets proof obligations generated by the Atelier-B framework in Why3 format. It should be used with a prelude defining the B Set theory.
Published: 14 May 2025
README
Alt-Ergo
Alt-Ergo is an open-source automatic solver of mathematical formulas designed for program verification. It is based on Satisfiability Modulo Theories (SMT). Solvers of this family have made impressive advances and became very popular during the last decade. They are now used is various domains such as hardware design, software verification and formal testing. It was developed at LRI, and is now improved and maintained at OCamlPro, and friendly collaboration is maintained with the Why3 development team.
You can try Alt-Ergo online. Also see the Alt-Ergo Users' Club.
Build status
next | main ------------ | ------------- 
" | 
"
Website
Alt-Ergo's website: https://alt-ergo.ocamlpro.com.
Documentation
See our general documentation, the API documentation and the developers documentation.
Download
We provide sources tarball of the latest release of Alt-Ergo. You can also find it on the GitHub's releases' page.
Alt-Ergo is available in the OCaml package manager opam with this command:
opam install alt-ergoCopyright
See the section LICENSE.
Build
See installation instructions section.
Contributing
Please refer to our contributing guidelines.
Support
See Alt-Ergo @ OCamlPro or contact us at alt-ergo@ocamlpro.com for more details.
Dependencies (4)
-
alt-ergo-parsers
= version -
alt-ergo-lib
= version -
alt-ergo
= version -
dune
>= "3.14"
Dev Dependencies (1)
-
odoc
with-doc
Used by
None