×

Alt-Ergo

swMATH ID: 4888
Software Authors: Sylvain Conchon, Evelyne Contejean
Description: Alt-Ergo is an automatic theorem prover dedicated to program verification. Alt-Ergo is based on CC(X) a congruence closure algorithm parameterized by an equational theory X. Currently, CC(X) can be instantiated by the empty equational theory and by the linear arithmetics. Alt-Ergo contains also a home made SAT-solver and an instantiation mechanism.
Homepage: http://ergo.lri.fr/
Operating Systems: Linux x86, Win32, Mac OS X
Related Software: Why3; z3; Coq; SIMPLIFY; KRAKATOA; CVC4; cvc3; Frama-C; Caduceus; VCC; Spec#; ACSL; KeY; Boogie; SMT-LIB; WhyML; SPASS; Isabelle/HOL; SPARK; JML
Cited in: 15 Publications

Citations by Year