Data Structures with Arithmetic Constraints: a Non-Disjoint Combination

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 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.
Type de document :
Rapport
[Research Report] RR-6963, INRIA. 2009, pp.23
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00397080
Contributeur : Christophe Ringeissen <>
Soumis le : vendredi 19 juin 2009 - 14:51:15
Dernière modification le : jeudi 11 janvier 2018 - 06:20:00
Document(s) archivé(s) le : lundi 15 octobre 2012 - 14:36:32

Fichier

RR-6963.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00397080, version 1

Citation

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〉

Partager

Métriques

Consultations de la notice

258

Téléchargements de fichiers

159