Combinable Extensions of Abelian Groups

version courte de inria-00383041 (INRIA RR-6920)International audienceThe 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 nondisjoint 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