Időpont: 2025.09.16. 10:15-12:00

Helyszín: IB023

Cím: Prof. Dirk Beyer (LMU) - Verification via Transformation

Abstract: After a short account of the history of software model checking, and the competition on software model checking, we come to the conclusion that we moved from a lack of tools to an abundance of tools in the past 25 years. Our vision is to use existing tools for verification as components or libraries, just as we nowadays use SMT solvers. New (meta) verification tools should form a new layer on top of the existing architectural layers. This requires clear interfaces and separation of concerns, as well as exchange formats for verification artifacts such as intermediate or partial results.  Only via the combination of verification tools and their technology, we can leverage all power we have available. We outline a few existing transformation approaches to illustrate that achieving the goal is possible in the near future.

Literature:

- Software Model Checking: 20 Years and Beyond

- The Transformation Game: Joining Forces for Verification

Bio: Dirk Beyer is Full Professor of Computer Science and has a Research Chair for Software and Computational-Systems Engineering at LMU Munich, Germany (since 2016). Before, he was Full Professor of Computer Science at University of Passau, Germany (2009-2016). He was Assistant and Associate Professor at Simon Fraser University, B.C., Canada (2006-2009), and Postdoctoral Researcher at EPFL in Lausanne, Switzerland (2004-2006) and at the University of California, Berkeley, USA (2003-2004), in the group of Tom Henzinger. Dirk Beyer holds a Dipl.-Inf. degree (1998) and a Dr. rer. nat. degree (2002) in Computer Science from the Brandenburg University of Technology in Cottbus, Germany. In 1998 he was Software Engineer with Siemens AG, SBS Dept. Major Projects in Dresden, Germany. His research focuses on models, algorithms, and tools for the construction and analysis of reliable software systems. He is architect, designer, and implementor of several successful tools. For example, CrocoPat is the first efficient interpreter for relational programming, CCVisu is a successful tool for visual clustering, and CPAchecker and BLAST are two well-known and successful software model checkers.