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 5 articles , 1 standard article )

Showing results 1 to 5 of 5.
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. Schnoebelen, Philippe: Lossy counter machines decidability cheat sheet (2010)
  5. Leroux, Jér^ome; Point, Gérald: TaPAS: the talence Presburger arithmetic suite (2009)