Skip to Main content Skip to Navigation

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 (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Complete list of metadata

Cited literature [25 references]  Display  Hide  Download
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Monday, May 11, 2009 - 6:20:13 PM
Last modification on : Saturday, October 16, 2021 - 11:26:06 AM
Long-term archiving on: : Monday, October 15, 2012 - 10:02:24 AM


Files produced by the author(s)


  • 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⟩



Record views


Files downloads