Combinable Extensions of Abelian Groups - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2009

Combinable Extensions of Abelian Groups

Résumé

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.
Fichier principal
Vignette du fichier
RR-6920.pdf (427.76 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00383041 , version 1 (11-05-2009)

Identifiants

  • HAL Id : inria-00383041 , version 1

Citer

Enrica Nicolini, Christophe Ringeissen, Michael Rusinowitch. Combinable Extensions of Abelian Groups. [Research Report] RR-6920, INRIA. 2009, pp.30. ⟨inria-00383041⟩
110 Consultations
210 Téléchargements

Partager

Gmail Facebook X LinkedIn More