Begin: Wednesday, 19th of February 2020 (4:00 pm)
Location: Warburger Str. 100, room O4.267
On February 19th, 2020, Prof. Dr. Dirk Beyer (LMU Munich) will give a talk about " Software Verification — An Overview of the State of the Art " in the context of the SFB 901.
Abstract:
This presentation provides an overview of the techniques that are used in state-of-the-art tools for software verification. The advance of technology in automatic verification is visible via annual comparative evaluations in the area (competitions). We will have a look at techniques and tools that are currently in use. SMT-based approaches play a particularly important role, such as predicate abstraction, k-induction, bounded model checking, but also heap graphs, intervals, explicit-state model checking, slicing, and symbolic execution.
One of the lessons learned is that the next break through is not expected to come from yet another new single algorithm, data structure, or technique, but from cooperation of techniques. Cooperative approaches for software verification work together on solving the problem. That is, approaches share information about the verification progress in an exchangeable way via clear interfaces - with other tools and with engineers - ideally in a black-box manner. We give an overview over existing combination techniques.
Bio: Dirk Beyer is Professor of Computer Science and has a Research Chair for Software Systems at LMU Munich, Germany. He was Full Professor at University of Passau (2009-2016), Assistant and Associate Professor at Simon Fraser University, B.C., Canada, 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 the 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.
