package alt-ergo-lib

  1. Overview
  2. Docs
The Alt-Ergo SMT prover library

Install

Dune Dependency

Authors

Maintainers

Sources

alt-ergo-2.5.1.tbz
sha256=9cf8d69a0e457a939b86aba2a18c6154faba51d387b42a361ece55d329dd601d
sha512=09694d18496ba1938daaa7b4e28e6b3d6811687dd3aaede17917f20511be9d8328394fac021af683d4c0217d4b030da9a60a5b9c14d968f1948735ea7ec52543

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/

Tags

org:OCamlPro

Published: 15 Sep 2023

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
Build Status (next) Build Status (main)

Website

Alt-Ergo's website: https://alt-ergo.ocamlpro.com.

Documentation

See our general documentation wich contains

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)

  1. camlzip >= "1.07"
  2. ppx_blob >= "0.7.2"
  3. stdlib-shims
  4. fmt >= "0.9.0"
  5. seq
  6. zarith >= "1.11"
  7. ocplib-simplex >= "0.5"
  8. dolmen_loop >= "0.9" & < "0.10"
  9. dolmen_type >= "0.9" & < "0.10"
  10. dolmen >= "0.9" & < "0.10"
  11. dune-build-info
  12. dune >= "3.0"
  13. ocaml >= "4.08.0"

Dev Dependencies (1)

  1. odoc with-doc

Used by (3)

  1. alt-ergo = "2.5.1"
  2. alt-ergo-parsers = "2.5.1"
  3. alt-ergo-plugin-ab-why3 = "2.5.1"

Conflicts (2)

  1. result < "1.5"
  2. ppxlib < "0.30.0"
OCaml

Innovation. Community. Security.