Satisfiability Modulo Non-Disjoint Combinations of Theories Connected via Bridging Functions

Paula Chocron 1, 2 Pascal Fontaine 3 Christophe Ringeissen 2
1 UBA - Universidad de Buenos Aires [Buenos Aires]
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
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
LORIA - FM - Department of Formal Methods , Inria Nancy - Grand Est, MPII - Max-Planck-Institut für Informatik
Abstract : The Nelson-Oppen combination method is ubiquitous in all Satisfiability Modulo Theories solvers. However, one of its major drawbacks is to be restricted to disjoint unions of theories. We investigate the problem of extending this combination method to particular non-disjoint unions of theories connected via bridging functions. This problem is of greatest interest for solving verification problems expressed in a combination of data structures and arithmetic. Our work can be viewed as a synthesis of previous contributions by different authors. We investigate here an approach by reduction from non-disjoint to disjoint combination which is particularly well-suited to combine the theory of absolutely free data structures with bridging functions over a target theory. We consider the problem of adapting the combination procedure to get a satisfiability procedure for the standard interpretations of the data structure. We present an enumeration procedure that allows us to revisit the case of lists with length.
Keywords : Satisfiability Modulo Theories bridging function combination method
Document type :
Conference papers
Liste complète des métadonnées
https://hal.inria.fr/hal-01087218
Contributor : Christophe Ringeissen <>
Submitted on : Tuesday, November 25, 2014 - 3:45:35 PM
Last modification on : Wednesday, April 17, 2019 - 4:06:02 PM

Identifiers

  • HAL Id : hal-01087218, version 1

Collections

INRIA | UNIV-FCOMTE | UNIV-LORRAINE | UNIV-BM | FEMTO-ST | UNIV-BM-THESE | LORIA-FM | LORIA

Citation

Paula Chocron, Pascal Fontaine, Christophe Ringeissen. Satisfiability Modulo Non-Disjoint Combinations of Theories Connected via Bridging Functions. Workshop on Automated Deduction: Decidability, Complexity, Tractability, ADDCT 2014. Held as Part of the Vienna Summer of Logic, affiliated with IJCAR 2014 and RTA 2014, Silvio Ghilardi, Ulrike Sattler, Viorica Sofronie-Stokkermans, Jul 2014, Vienna, Austria. ⟨hal-01087218⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

279

Contact


archive-ouverte@inria.fr