alt-ergo
| Author | Alt-Ergo developers | |||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| License | CeCILL-C | |||||||||||||||||||||
| Homepage | http://alt-ergo.ocamlpro.com/ | |||||||||||||||||||||
| Issue Tracker | https://github.com/OCamlPro/alt-ergo/issues | |||||||||||||||||||||
| Maintainer | alt-ergo@ocamlpro.com | |||||||||||||||||||||
| Dependencies |
| |||||||||||||||||||||
| Available | ocaml-version >= "4.01.0" | |||||||||||||||||||||
| Published | Nov 21, 2016 | |||||||||||||||||||||
| Source [http] | http://alt-ergo.ocamlpro.com/http/alt-ergo-1.30/alt-ergo-1.30.tar.gz c7100ebd625fbd7d3e5247dbac689748 | |||||||||||||||||||||
| Statistics | Installed 253 times last month. | |||||||||||||||||||||
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/alt-ergo/alt-ergo.1.30/opam | |||||||||||||||||||||
Alt-Ergo, an SMT Solver for Software Verification
Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools such as Frama-C, SPARK, Why3, Atelier-B and Caveat.
This package provides the command-line version of Alt-Ergo.
usage: alt-ergo [options] <file.why>
| Necessary for | ||
|---|---|---|
| fm-simplex-plugin | ||
| >= 1.30 | ||
| frama-c | ||
| >= 20160502 | ||
| profiler-plugin | ||
| >= 1.30 | ||
| satML-plugin | ||
| >= 1.30 | ||
| why | ||
| & | >= 2.32 | |
| < 2.35 | ||
| why3 | ||
| < 0.85 | ||
