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
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Demri, Stéphane; Dhar, Amit Kumar; Sangnier, Arnaud: Equivalence between model-checking flat counter systems and Presburger arithmetic (2018)
- 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)