@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",