On Thursday 14 November 2013, 11:00-12:00 room B31 of INRIA Lille, Pascal Fontaine (LORIA Nancy) will give a talk on “SMT and combination of theories”.
Abstract:
Satisfiability Modulo Theories (SMT) solvers are used in an increasing number of applications. After a brief presentation of the internals of SMT solvers, we will review some results on combining theories. Combination of theories is at the core of SMT solvers, allowing several decision procedures (and notably for the theory for linear arithmetic and for the theory for uninterpreted functions) to cooperate to decide the satisfiability of sets of literals in the union of the languages. Combining decision procedures is not always possible, but for disjoint languages, many positive results exist.
