Skip to Main content Skip to Navigation
New interface
Conference papers

On Superposition-Based Satisfiability Procedures and their Combination

Hélène Kirchner 1 Silvio Ranise 2 Christophe Ringeissen 2 Duc-Khanh Tran 1, 2 
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 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 : We study how to efficiently combine satisfiability procedures built by using a superposition calculus with satisfiability procedures for theories, for which the superposition calculus may not apply (e.g., for various decidable fragments of Arithmetic). Our starting point is the Nelson-Oppen combination method, where satisfiability procedures cooperate by exchanging entailed (disjunction of) equalities between variables. We show that the superposition calculus deduces sufficiently many such equalities for convex theories (e.g., the theory of equality and the theory of lists) and disjunction of equalities for non-convex theories (e.g., the theory of arrays) to guarantee the completeness of the combination method. Experimental results on proof obligations extracted from the certification of auto-generated aerospace software confirm the efficiency of the approach. Finally, we show how to make satisfiability procedures built by superposition both incremental and resettable by using a hierarchic variant of the Nelson-Oppen method.
Document type :
Conference papers
Complete list of metadata
Contributor : Christophe Ringeissen Connect in order to contact the contributor
Submitted on : Friday, November 4, 2005 - 1:44:37 PM
Last modification on : Friday, January 21, 2022 - 3:09:01 AM

Links full text



Hélène Kirchner, Silvio Ranise, Christophe Ringeissen, Duc-Khanh Tran. On Superposition-Based Satisfiability Procedures and their Combination. 2nd International Colloquium on Theoretical Aspects of Computing - ICTAC'05, Oct 2005, Hanoi/Vietnam, pp.594--608, ⟨10.1007/11560647⟩. ⟨inria-00000586⟩



Record views