FMAS 2023 | Prof. Erika Ábrahám - SMT: Something you Must Try

Описание: This is a recording of an invited talk at the Fifth Workshop on Formal Methods for Autonomous Systems (FMAS 2023) joint with iFM 2023.

FMAS brings together researchers working on a range of techniques for the formal verification of autonomous systems. Details of FMAS 2023, including the link to the workshop proceedings can be found at: https://fmasworkshop.github.io/FMAS2023/

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. These tools are general purpose and as off-the-shelf solvers, their usage is truly integrated. A typical application encodes real-world problems as logical formulas, whose solutions can be decoded to solutions of the real-world problem. In this talk we give some insights into the mechanisms of SMT solving, discuss some areas of application, and present a novel application from the domain of simulation.

Biography: Prof. 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. Furthermore, she is also active in the development of algorithms and tools (solvers) for satisfiability checking.