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.

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

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

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