Skip to Main content Skip to Navigation
Journal articles

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 (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Journal articles
Complete list of metadatas
Contributor : Christophe Ringeissen <>
Submitted on : Friday, October 15, 2010 - 2:37:19 PM
Last modification on : Friday, January 15, 2021 - 3:24:33 AM



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⟩



Record views