@InProceedings{Chocron3,
author = "Paula Chocron and Pascal Fontaine and Christophe
Ringeissen",
title = "A Rewriting Approach to the Combination of Data
Structures with Bridging Theories",
booktitle = frocos,
pages = "275--290",
doi = "10.1007/978-3-319-24246-0_17",
editor = "Carsten Lutz and Silvio Ranise",
series = lncs,
volume = "9322",
publisher = "Springer",
year = "2015",
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.",
URL = "Chocron3.pdf",
}
% URL = "http://dx.doi.org/10.1007/978-3-319-24246-0_17",