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 optimization, planning and controller synthesis, just to mention a few well-known areas. In this talk, we give a historical overview of this development, describe our own solver SMT-RAT, and discuss some applications and potentials.

About Erika Ábrahám

Erika graduated at the Christian-Albrechts-University Kiel (Germany), and received her Ph.D. from the University of Leiden (The Netherland) for her work on the development and application of deductive proof systems for concurrent programs. Then she moved to the Albert-Ludwigs-University Freiburg (Germany), where she started to work on the development and application of SAT and SMT solvers. Currently she is a professor at RWTH Aachen University (Germany), with main research focus on SMT solving for real and integer arithmetic, and formal methods for probabilistic and hybrid systems.

Note for Students

The lecture series of research talks by the visiting professors of the Vienna PhD School of Informatics can also be credited as an elective course for students of Master’s programs of computer science: LVA 195.072 Current Trends in Computer Science.

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.