Am Mittwoch, den 19.02.20 um 16:00 Uhr wird Prof. Dr. Dirk Beyer von der Ludwig-Maximilians-Universität München einen Vortrag zum Thema „Software Verification – An Overview of the State of the Art“ in O4.267 halten.
Dirk Beyer ist Professor der Informatik und Inhaber des Lehrstuhls für Softwaresysteme an der LMU München. Zuvor war er von 2009 bis 2016 Lehrstuhlinhaber an der Universität Passau. Sein Studium der Informatik und die anschließende Promotion erfolgten an der Technischen Universität Cottbus. 2003 sammelte er als Postdoctoral Researcher Erfahrungen an der University of California, Berkeley (USA), bevor er dann von 2004 bis 2006 an der Eidgenössischen Technischen Hochschule Lausanne in der Schweiz forschte. 2006 trat er seine erste Stelle als Professor an der kanadischen Simon Fraser University in Vancouver an.
Seine Forschungsschwerpunkte sind Modelle, Algorithmen und Tools für die Errichtung und Analyse von verlässlichen Softwaresystemen. Mit CrocoPat entwickelte er den ersten effizienten Interpreter für relationale Programmierung und arbeitete unter anderem am Verifikationswerkzeug für die Software BLAST.
In seinem Abstract erläutert er seinen Vortragsgegenstand:
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.
Alle Interessierten sind herzlich eingeladen!
