Satisfiability Modulo Theories for Arithmetic Problems

Abstract: Satisfiability Modulo Theories (SMT) solving has grown to be a very successful solving paradigm, powering software and hardware verification, symbolic execution, test-case generation, synthesis, planning, scheduling and optimization tasks. One of the theories in SMT solving is nonlinear real arithmetic which opens immediate connections to the computer algebra community that has long known this theory as the theory of the reals. This talk presents approaches for this theory that are used in the SMT community and discusses some existing and possible future collaboration between the SMT and computer algebra communities.

mathematical softwaresymbolic computationMathematics

Audience: learners

( slides | video )

Global Virtual SageDays 112.358