package alt-ergo-lib
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=02c1e89398badafa89e612bc5d1883f2133a250685bf774cc5901c5581229bac
sha512=9f565c3f0d17328465832b8b107f048d67225bee23b83c7b02e820796201ca96cdb99574ff50c619badaadd5274b5c128d8f30e7532d44a1ee061a7e2d5d318d
Description
This is the core library used in the Alt-Ergo SMT solver.
Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro.
See more details on http://alt-ergo.ocamlpro.com/
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 wich contains
the usage section for information on how to use Alt-Ergo.
A section about input file format supported by Alt-Ergo.
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-ergo
Copyright
Alt-Ergo is freely available for non-commercial uses (such as academic and exploratory trials) under the OCamlPro non-commercial license 1.0.
For commercial use, see the Alt-Ergo Users' Club. Club members with adequate membership can have access to Alt-Ergo under the Apache Software License version 2.0. See the license section for more detail.
Build
See installing informations 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 (13)
-
camlzip
>= "1.07"
-
ppx_blob
>= "0.7.2"
- stdlib-shims
-
fmt
>= "0.9.0"
- seq
-
zarith
>= "1.11"
-
ocplib-simplex
>= "0.5"
-
dolmen_loop
= "0.9"
-
dolmen_type
= "0.9"
-
dolmen
= "0.9"
- dune-build-info
-
dune
>= "3.0"
-
ocaml
>= "4.08.0"
Dev Dependencies (1)
-
odoc
with-doc
Used by (3)
-
alt-ergo
= "2.5.4"
-
alt-ergo-parsers
= "2.5.4"
-
alt-ergo-plugin-ab-why3
= "2.5.4"