A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited

Paula Chocron 1 Pascal Fontaine 2 Christophe Ringeissen 3
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : The Nelson-Oppen combination method is ubiquitous in 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. The motivation is, e.g., to solve verification problems expressed in a combination of data structures connected to arithmetic with bridging functions such as the length of lists and the size of trees. We present a sound and complete combination procedure à la Nelson-Oppen for the theory of absolutely free data structures, including lists and trees. This combination procedure is then refined for standard interpretations. The resulting theory has a nice politeness property, enabling combinations with arbitrary decidable theories of elements.
Type de document :
Communication dans un congrès
Amy P. Felty and Aart Middeldorp. 25th International Conference on Automated Deduction, CADE-25, Aug 2015, Berlin, Germany. Springer, 9195, pp.419-433, 2015, Lecture Notes in Computer Science. 〈10.1007/978-3-319-21401-6_29〉
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01157898
Contributeur : Christophe Ringeissen <>
Soumis le : jeudi 28 mai 2015 - 18:25:58
Dernière modification le : jeudi 22 septembre 2016 - 14:31:59
Document(s) archivé(s) le : lundi 24 avril 2017 - 17:47:15

Fichier

bridging-nd-compact.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Paula Chocron, Pascal Fontaine, Christophe Ringeissen. A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited. Amy P. Felty and Aart Middeldorp. 25th International Conference on Automated Deduction, CADE-25, Aug 2015, Berlin, Germany. Springer, 9195, pp.419-433, 2015, Lecture Notes in Computer Science. 〈10.1007/978-3-319-21401-6_29〉. 〈hal-01157898〉

Partager

Métriques

Consultations de
la notice

460

Téléchargements du document

143