SMT: Something you Must Try

Mercoledì 29 luglio 2026 | 16:30
Dipartimento di Elettronica, Informazione e Bioingegneria - Politecnico di Milano
Sala Schiavoni (Ed. 20A)

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

Sommario

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.

Biografia

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.