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: 18 Oct 2023
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.
Alt-Ergo's website: https://alt-ergo.ocamlpro.com.
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.
Alt-Ergo is available in the OCaml package manager opam with this command:
opam install alt-ergo
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.
See installing informations section.
Please refer to our contributing guidelines.