Session 9. Satisfiability Checking and Symbolic Computation


Aim and Scope

Software tools for checking the satisfiability of real-algebraic formulas play an important role in a wide range of applications. Such tools are being developed in Mathematics in form of computer algebra systems as well as in Computer Science as SAT-modulo-theories (SMT) solvers. With this topical session we want to strengthen the exchange between these areas, with presentations about algorithms and software tools from both domains and success stories about how the two communities can profit from achievements of each other.