Combinable Extensions of Abelian Groups

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 : The design of decision procedures for combinations of theories sharing some arithmetic fragment is a challenging problem in verification. One possible solution is to apply a combination method à la Nelson-Oppen, like the one developed by Ghilardi for unions of non-disjoint theories. We show how to apply this non-disjoint combination method with the theory of abelian groups as shared theory. We consider the completeness and the effectiveness of this non-disjoint combination method. For the completeness, we show that the theory of abelian groups can be embedded into a theory admitting quantifier elimination. For achieving effectiveness, we rely on a superposition calculus modulo abelian groups that is shown complete for theories of practical interest in verification.
Type de document :
Rapport
[Research Report] RR-6920, INRIA. 2009, pp.30
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00383041
Contributeur : Christophe Ringeissen <>
Soumis le : lundi 11 mai 2009 - 18:20:13
Dernière modification le : jeudi 11 janvier 2018 - 06:20:00
Document(s) archivé(s) le : lundi 15 octobre 2012 - 10:02:24

Fichier

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

Identifiants

  • HAL Id : inria-00383041, version 1

Citation

Enrica Nicolini, Christophe Ringeissen, Michael Rusinowitch. Combinable Extensions of Abelian Groups. [Research Report] RR-6920, INRIA. 2009, pp.30. 〈inria-00383041〉

Partager

Métriques

Consultations de la notice

222

Téléchargements de fichiers

123