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