A Rewriting Approach to the Combination of Data Structures with Bridging Theories

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 : We introduce a combination method à la Nelson-Oppen to solve the satisfiability problem modulo a non-disjoint union of theories connected with bridging functions. The combination method is particularly useful to handle verification conditions involving functions defined over inductive data structures. We investigate the problem of determining the data structure theories for which this combination method is sound and complete. Our completeness proof is based on a rewriting approach where the bridging function is defined as a term rewrite system, and the data structure theory is given by a basic congruence relation. Our contribution is to introduce a class of data structure theories that are combinable with a disjoint target theory via an inductively defined bridging function. This class includes the theory of equality, the theory of absolutely free data structures, and all the theories in between. Hence, our non-disjoint combination method applies to many classical data structure theories admitting a rewrite-based satisfiability procedure.
Type de document :
Communication dans un congrès
Carsten Lutz and Silvio Ranise. Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Sep 2015, Wroclaw, Poland. Springer, 9322, pp.275--290, Lecture Notes in Computer Science. 〈10.1007/978-3-319-24246-0_17〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01206187
Contributeur : Christophe Ringeissen <>
Soumis le : lundi 28 septembre 2015 - 15:20:30
Dernière modification le : jeudi 22 septembre 2016 - 14:31:57
Document(s) archivé(s) le : mardi 29 décembre 2015 - 10:34:22

Fichier

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

Identifiants

Citation

Paula Chocron, Pascal Fontaine, Christophe Ringeissen. A Rewriting Approach to the Combination of Data Structures with Bridging Theories. Carsten Lutz and Silvio Ranise. Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Sep 2015, Wroclaw, Poland. Springer, 9322, pp.275--290, Lecture Notes in Computer Science. 〈10.1007/978-3-319-24246-0_17〉. 〈hal-01206187〉

Partager

Métriques

Consultations de la notice

204

Téléchargements de fichiers

73