Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator

Enrica Nicolini 1 Christophe Ringeissen 1 Michael Rusinowitch 1
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present some decidability results for the universal fragment of theories modeling data structures and endowed with arithmetic constraints. More precisely, all the theories taken into account extend a theory that constrains the function symbol for the successor. A general decision procedure is obtained, by devising an appropriate calculus based on superposition. Moreover, we derive a decidability result for the combination of the considered theories for data structures and some fragments of arithmetic by applying a general combination schema for theories sharing a common subtheory. The effectiveness of the resulting algorithm is ensured by using the proposed calculus and a careful adaptation of standard methods for reasoning about arithmetic, such as Gauss elimination, Fourier-Motzkin elimination and Groebner bases computation.
Type de document :
Article dans une revue
Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2010, 105 (1-2), pp.163--187. 〈10.3233/FI-2010-362〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00526683
Contributeur : Christophe Ringeissen <>
Soumis le : vendredi 15 octobre 2010 - 14:37:19
Dernière modification le : jeudi 11 janvier 2018 - 06:20:00

Identifiants

Citation

Enrica Nicolini, Christophe Ringeissen, Michael Rusinowitch. Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator. Fundamenta Informaticae, Polskie Towarzystwo Matematyczne, 2010, 105 (1-2), pp.163--187. 〈10.3233/FI-2010-362〉. 〈inria-00526683〉

Partager

Métriques

Consultations de la notice

220