TaPAS

TaPAS: the talence Presburger arithmetic suite TaPAS is a suite of libraries dedicated to FO(ℝ,ℤ,+,≤). The suite provides (1) the application programming interface Genepi for this logic with encapsulations of many classical solvers, (2) the BDD-like library SaTAF used for encoding Presburger formulae to automata, and (3) the very first implementation of an algorithm decoding automata to Presburger formulae.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 7 articles , 1 standard article )

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

  1. Demri, Stéphane; Dhar, Amit Kumar; Sangnier, Arnaud: Equivalence between model-checking flat counter systems and Presburger arithmetic (2018)
  2. Barrett, Clark; Demri, Stéphane; Deters, Morgan: Witness runs for counter machines (2013)
  3. Bertrand, N.; Schnoebelen, P.: Computable fixpoints in well-structured symbolic model checking (2013)
  4. Heußner, Alexander; Le Gall, Tristan; Sutre, Grégoire: McScM: a general framework for the verification of communicating machines (2012) ioport
  5. Bersani, Marcello M.; Demri, Stéphane: The complexity of reversal-bounded model-checking (2011)
  6. Schnoebelen, Philippe: Lossy counter machines decidability cheat sheet (2010)
  7. Leroux, Jér^ome; Point, Gérald: TaPAS: the talence Presburger arithmetic suite (2009)