Introduction

The GENEPI Library allows the manipulation of Presburger definable sets by means of dynamically loaded solvers. The aim of the GENEPI library is twofold:

• On one hand it can be used as a solver of Presburger formulas and, thus, use in softwares needing such tool. Basically GENEPI was designed for the model-checker called FASTer (http://www.lsv.ens-cachan.fr/fast/) that implements acceleration techniques based on symbolic representation of state spaces for infinite systems.
• On the other hand it can be used to compare solver performances. There currently exists 6 solvers compliant with GENEPI:
  • LASH: http://www.montefiore.ulg.ac.be/~boigelot/research/lash/
  • LIRA: http://lira.gforge.avacs.org/
  • MONA: http://www.brics.dk/~mona/
  • Omega: http://www.cs.umd.edu/projects/omega/
  • PresTAF: http://altarica.labri.fr/wiki/tools:tapas:prestaf
  • PPL: http://www.cs.unipr.it/ppl/
  All plugins can be downloaded on http://tapas.labri.fr/.