From 6af9acff125ca984cdbf1857cba7f00b3de1c5e0 Mon Sep 17 00:00:00 2001 From: Landon Taylor Date: Fri, 13 Jun 2025 14:28:33 -0600 Subject: [PATCH] add alt-ergo. Closes #1 --- tools/sat-smt/alt-ergo.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 tools/sat-smt/alt-ergo.md diff --git a/tools/sat-smt/alt-ergo.md b/tools/sat-smt/alt-ergo.md new file mode 100644 index 0000000..a563354 --- /dev/null +++ b/tools/sat-smt/alt-ergo.md @@ -0,0 +1,22 @@ ++++ +date = 2025-06-07 +draft = false +title = 'Alt-Ergo' +subtitle = 'SMT Solver' +links = [ + { title = "Homepage", url = "https://alt-ergo.ocamlpro.com/", icon = 'fa-solid fa-home' }, + { title = "Source Code", url = "https://github.com/ocamlpro/alt-ergo", icon = 'fa-brands fa-github' }, + { title = "Playground", url = "https://try-alt-ergo.ocamlpro.com/", icon = 'fa-solid fa-gamepad' } +] +applications = ['SMT Solver'] +developers = ['OCaml Pro'] +licenses = ['OCamlPro-Non-Commercial'] +inputs = ['SMTLIB2', 'Alt-Ergo'] +interfaces = ['CLI', 'Online'] +maintenance = ['Actively Maintained'] +# techniques = ['CDCL'] +# publications = [''] ++++ + + +Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools such as Frama-C, SPARK, Why3, Atelier-B and Caveat. \ No newline at end of file