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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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 metadatas

https://hal.inria.fr/inria-00000586
Contributor : Christophe Ringeissen <>
Submitted on : Friday, November 4, 2005 - 1:44:37 PM
Last modification on : Friday, July 6, 2018 - 3:06:10 PM

Identifiers

Citation

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⟩

Share

Metrics

Record views

233