Tuesday, May 17, 2016
Speaker: Erika Abraham
Venue: IST Austria
Satisfiability Checking aims to develop algorithms and tools for checking the satisfiability of existentially quantified logical formulas. For propositional logic, in the late ’90s impressive progress was made towards practically applicable solutions, resulting in powerful SAT solvers. Driven by this success, a new line of research started to enrich propositional SAT solving with solver modules for different theories. Nowadays, sophisticated SAT-modulo-theories (SMT) solvers are available for, e.g., equality logic with uninterpreted functions, bit-vector arithmetic, array theory, floating point arithmetic, and real and integer arithmetic. SAT and SMT solvers are now at the heart of many techniques for the analysis of programs and probabilistic, timed, hybrid and cyber-physical systems, for test-case generation, for solving large combinatorial problems and complex scheduling tasks, for product design optimisation, planning and controller synthesis, just to mention a few well-known areas.
In this talk we first give an introduction to the theoretical foundations of SMT solving, and mention some examples for the successful employment of SMT solvers in different software technologies. Focussing on non-linear arithmetic theories, we discuss the connection between the areas of Satisfiability Checking and Symbolic Computation and illustrate the embedding of arithmetic decision procedures in SMT solvers on the example of the Cylindrical Algebraic Decomposition method. Besides SMT-solving approaches for non-linear real arithmetic, we also discuss opportunities for moving from the real to the integer domain.