Combinable Extensions of Abelian Groups - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2009

Combinable Extensions of Abelian Groups

(1) , (1) , (1)


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
Origin : Files produced by the author(s)

Dates and versions

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


  • HAL Id : inria-00383041 , version 1


Enrica Nicolini, Christophe Ringeissen, Michael Rusinowitch. Combinable Extensions of Abelian Groups. [Research Report] RR-6920, INRIA. 2009, pp.30. ⟨inria-00383041⟩
107 View
202 Download


Gmail Facebook Twitter LinkedIn More