Alt-Ergo

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.


References in zbMATH (referenced in 13 articles )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. Chaudhari, Dipak L.; Damani, Om: Combining top-down and bottom-up techniques in program derivation (2015)
  2. McCormick, John W.; Chapin, Peter C.: Building high integrity applications with SPARK (2015)
  3. Dockins, Robert; Tolmach, Andrew: suppl: a flexible language for policies (2014)
  4. Brumley, Billy B.; Barbosa, Manuel; Page, Dan; Vercauteren, Frederik: Practical realisation and elimination of an ECC-related software bug attack (2012)
  5. Conchon, Sylvain; Contejean, Evelyne; Iguernelala, Mohamed: Canonized rewriting and ground AC completion modulo Shostak theories: design and implementation (2012)
  6. Chapman, Roderick; Botcazou, Eric; Wallenburg, Angela: SPARKSkein: a formal and fast reference implementation of Skein (2011) ioport
  7. Conchon, Sylvain; Contejean, Evelyne; Iguernelala, Mohamed: Canonized rewriting and ground AC completion modulo Shostak theories (2011)
  8. Dross, Claire; Filli^atre, Jean-Christophe; Moy, Yannick: Correct code containing containers (2011)
  9. Frade, Maria João; Pinto, Jorge Sousa: Verification conditions for source-level imperative programs (2011)
  10. Moy, Yannick; Marché, Claude: Modular inference of subprogram contracts for safety checking (2010)
  11. Nguyen, An N.; Quan, Tho T.; Nguyen, Phung H.; Bui, Thang H.: COMBINE: a tool on combined formal methods for bindingly verification (2010) ioport
  12. Conchon, Sylvain; Contejean, Evelyne; Kanig, Johannes; Lescuyer, Stéphane: \ssfCC(X): semantic combination of congruence closure with solvable theories (2008)
  13. Conchon, Sylvain; Filli^atre, Jean-Christophe: Semi-persistent data structures (2008)