×

zbMATH — the first resource for mathematics

TaPAS: the talence Presburger arithmetic suite. (English) Zbl 1234.03002
Kowalewski, Stefan (ed.) et al., Tools and algorithms for the construction and analysis of systems. 15th international conference, TACAS 2009, held as part of the joint European conferences on theory and practice of software, ETAPS 2009, York, UK, March 22–29, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-00767-5/pbk). Lecture Notes in Computer Science 5505, 182-185 (2009).
Summary: TaPAS is a suite of libraries dedicated to \(\text{FO}\,(\mathbb R,\mathbb Z, +, \leq)\). 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.
For the entire collection see [Zbl 1157.68007].

MSC:
03-04 Software, source code, etc. for problems pertaining to mathematical logic and foundations
03D05 Automata and formal grammars in connection with logical questions
03F30 First-order arithmetic and fragments
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
TaPAS; LIRA
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Becker, B., Dax, C., Eisinger, J., Klaedtke, F.: LIRA: Handling constraints of linear arithmetics over the integers and the reals. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 307–310. Springer, Heidelberg (2007) · Zbl 05216241
[2] Bardin, S., Leroux, J., Point, G.: FAST extended release. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 63–66. Springer, Heidelberg (2006) · Zbl 05187414
[3] Couvreur, J.-M.: A BDD-like implementation of an automata package. In: Domaratzki, M., Okhotin, A., Salomaa, K., Yu, S. (eds.) CIAA 2004. LNCS, vol. 3317, pp. 310–311. Springer, Heidelberg (2005) · Zbl 1115.68425
[4] Leroux, J.: A polynomial time presburger criterion and synthesis for number decision diagrams. In: LICS, pp. 147–156. IEEE Comp. Soc., Los Alamitos (2005)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.