Compare commits

..

1 Commits

Author SHA1 Message Date
6af9acff12 add alt-ergo. Closes #1 2025-06-13 14:28:33 -06:00

22
tools/sat-smt/alt-ergo.md Normal file
View File

@@ -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 = ['']
+++
<!-- {{<inactive year="2024">}} -->
Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools such as Frama-C, SPARK, Why3, Atelier-B and Caveat.