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 all top 5 Cited by 30 Authors 5 Conchon, Sylvain 3 Contejean, Evelyne 2 Filliâtre, Jean-Christophe 2 Iguernelala, Mohamed 2 Marché, Claude 2 Moy, Yannick 1 Barbosa, Manuel 1 Brumley, Billy Bob 1 Chapin, Peter C. 1 Chaudhari, Dipak L. 1 Cristiá, Maximiliano 1 Damani, Om P. 1 Dross, Claire 1 Frade, Maria João 1 Groves, Lindsay J. 1 Iguernlala, Mohamed 1 Ishii, Daisuke 1 Jeannerod, Nicolas 1 Kanig, Johannes 1 Lescuyer, Stéphane 1 McCormick, John W. 1 Page, Dan 1 Pearce, David J. 1 Pinto, Jorge Sousa 1 Rossi, Gianfranco 1 Roux, Pierre 1 Treinen, Ralf 1 Utting, Mark 1 Vercauteren, Frederik 1 Yabu, Tomohito Cited in 5 Serials 1 Journal of Computational and Applied Mathematics 1 Journal of Symbolic Computation 1 Journal of Automated Reasoning 1 Logical Methods in Computer Science 1 Computer Science Review Cited in 5 Fields 14 Computer science (68-XX) 4 Mathematical logic and foundations (03-XX) 1 Numerical analysis (65-XX) 1 Operations research, mathematical programming (90-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year