• Slipshow. An engine for displaying an enhanced version of slides (called slips). See the documentation. Developed by Paul-Elliot Anglès d’Auriac. NEW
  • CsP: superposition-based abduction (by S. Tourret).
  • GPID: abduction modulo theories (part of the Abdulot framework). Implemented by Y. Sellami.
  • Ilinva: a system to generate loop invariants (uses GPID and Why3). Implemented by Y. Sellami.
  • DEI: theorem proving with iterated terms. Implemented by H. Bensaid.
  • ECS: constraint solving in the empty theory.
  • FISH: A Flat Instantiation ScHeme.
  • RegSTAB: a SAT-Solver extended with the possibility to handle formulae patterns. Implemented by V. Aravantinos.