SMT: Something you Must Try

Wednesday, July 29, 2026 | 4:30 PM
Department of Electronics, Information and Bioengineering - Politecnico di Milano
Schiavoni Room (Bldg. 20A)

Speaker: Erika Ábrahám (RWTH Aachen University, Germany)

Abstract

SMT (Satisfiability Modulo Theories) solving is a technology for the fully automated solution of logical formulas. Due to their impressive efficiency, SMT solvers are nowadays frequently used in a wide variety of applications. A typical application encodes real-world problems as logical formulas, uses SMT solvers to solve the formulas, and decodes the solutions of the formula to solutions for the real-world problem.

In this talk we give some insights into the mechanisms of SMT solving and discuss some areas of application.

Short Bio

Erika Ábrahám was born in Hungary and moved to Germany to study Computer Science at the University of Kiel. After her diploma studies, she started to work on deductive proof systems and received her Ph.D. from the University of Leiden in 2005. As a postdoctoral researcher, she was active in different areas of formal methods at the University of Freiburg and at Forschungszentrum Jülich before she was appointed a junior professorship at RWTH Aachen University in 2008, and became a full professor in 2013. Ábrahám's main research interests are formal methods for the synthesis and analysis of discrete, hybrid, and probabilistic systems, including the development and usage of SMT solvers as general-purpose tools.