Open for all UnRAVeL Members: Informatics Europe Web-Seminar: SMT Solving: Past, Present and Future

Thursday, October 21, 2021, 5:00pm

Location: Online Session
Registration

Speaker: Prof. Dr. Erika Abraham

 

Abstract: 

Since the development of the first computer algebra systems in the '60s, automated decision procedures for checking the satisfiability of logical formulas gained more and more importance.

Besides symbolic computation techniques, some major achievements were made in the '90s in the relatively young area of satisfiability checking, and resulted in powerful SAT and SAT-modulo-theories (SMT) solvers.

Nowadays, these sophisticated tools are 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 give a historical overview of this development, describe shortly our own solver SMT-RAT, and discuss applications and some fascinating new developments for checking the satisfiability of real-arithmetic formulas.