Data Structures with Arithmetic Constraints: a Non-Disjoint Combination - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Reports (Research Report) Year : 2009

Data Structures with Arithmetic Constraints: a Non-Disjoint Combination

Abstract

We apply an extension of the Nelson-Oppen combination method to develop a decision procedure for the non-disjoint union of theories modeling data structures with a counting operator and fragments of arithmetic. We present some data structures and some fragments of arithmetic for which the combination method is complete and effective. To achieve effectiveness, the combination method relies on particular procedures to compute sets that are representative of all the consequences over the shared theory. We show how to compute these sets by using a superposition calculus for the theories of the considered data structures and various solving and reduction techniques for the fragments of arithmetic we are interested in, including Gauss elimination, Fourier-Motzkin elimination and Groebner bases computation.
Fichier principal
Vignette du fichier
RR-6963.pdf (360.82 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00397080 , version 1 (19-06-2009)

Identifiers

  • HAL Id : inria-00397080 , version 1

Cite

Enrica Nicolini, Christophe Ringeissen, Michael Rusinowitch. Data Structures with Arithmetic Constraints: a Non-Disjoint Combination. [Research Report] RR-6963, INRIA. 2009, pp.23. ⟨inria-00397080⟩
139 View
258 Download

Share

Gmail Facebook X LinkedIn More