TaPAS: The Talence Presburger Arithmetic Suite

TAPAS is a suite of libraries dedicated to FO (R, Z, +, ≤). 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. 1 The Mixed Additive Theory The automatic verification of reactive systems is a major field of research. These systems are usually modeled with variables taking values in some infinite domains. Popular approaches for analyzing these models are based on decision procedures adapted to the variables domains. For numerical variables the mixed additive theory FO (R, Z, +, ≤) provides a natural logic to express linear constraints between integral variables and real variables. This logic has positive aspects: it is decidable and actually many solvers implement decision procedures for the full logic or some sub-logics like t...

• Type: Conference
• Year: 2009
• Where: TACAS
• Authors: Jérôme Leroux, Gérald Point
• Keywords: Algorithms, Mixed Additive Theory, Presburger Formulae, TACAS 2009, TAPAS