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.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- McCormick, John W.; Chapin, Peter C.: Building high integrity applications with SPARK (2015)
- Dockins, Robert; Tolmach, Andrew: suppl: a flexible language for policies (2014)
- Conchon, Sylvain; Contejean, Evelyne; Iguernelala, Mohamed: Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation (2012)
- Chapman, Roderick; Botcazou, Eric; Wallenburg, Angela: SPARKSkein: A formal and fast reference implementation of Skein (2011)
- Conchon, Sylvain; Contejean, Evelyne; Iguernelala, Mohamed: Canonized rewriting and ground AC completion modulo Shostak theories (2011)
- Dross, Claire; Filli^atre, Jean-Christophe; Moy, Yannick: Correct code containing containers (2011)
- Frade, Maria João; Pinto, Jorge Sousa: Verification conditions for source-level imperative programs (2011)
- Moy, Yannick; Marché, Claude: Modular inference of subprogram contracts for safety checking (2010)
- Nguyen, An N.; Quan, Tho T.; Nguyen, Phung H.; Bui, Thang H.: COMBINE: a tool on combined formal methods for bindingly verification (2010)