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 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 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.
Document type :
Conference papers
Complete list of metadatas

https://hal.inria.fr/inria-00428077
Contributor : Christophe Ringeissen <>
Submitted on : Wednesday, October 28, 2009 - 5:23:28 PM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM

Links full text

Identifiers

Citation

Enrica Nicolini, Christophe Ringeissen, Michael Rusinowitch. Combinable Extensions of Abelian Groups. 22nd International Conference on Automated Deduction - CADE-22, Aug 2009, Montreal, Canada. pp.51-66, ⟨10.1007/978-3-642-02959-2_4⟩. ⟨inria-00428077⟩

Share

Metrics

Record views

179