@InProceedings{Chocron4,
  author =       "Paula Chocron and Pascal Fontaine and Christophe
                 Ringeissen",
  title =        "A Polite Non-Disjoint Combination Method: Theories
                 with Bridging Functions Revisited",
  booktitle =    cade,
  pages =        "419--433",
  doi =          "10.1007/978-3-319-21401-6_29",
  editor =       "Amy P. Felty and Aart Middeldorp",
  series =       "Lecture Notes in Computer Science",
  volume =       "9195",
  publisher =    "Springer",
  year =         "2015",
  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.",
  URL =          "Chocron4.pdf",
}

%  URL =          "http://dx.doi.org/10.1007/978-3-319-21401-6_29",