Beschreibung
Abstract:
Im Bereich der Verifikation von Software gibt es leider eine große Kluft zwischen dem aktuellen Stand der Forschung und der angewandten Technologie in der industriellen Praxis. Wie können wir eine Brücke über diese Kluft bauen?
Eine Möglichkeit wäre, dass Firmen an die Forschungsgruppen herantreten mit Problemstellungen, für die eine neue Verifikationstechnologie benötigt wird. Allerdings scheitert dieses Vorhaben oft schon an der Geheimhaltungsschranke.
Eine andere Möglichkeit wäre, dass die Forscher den aktuellen Stand der Technik für die Entwickler und Qualitätsingenieure in der Praxis in bequem konsumierbarer Form anbieten.
Die Lösungsidee dafür ist die "International Competition on Software Verification (SV-COMP)", bei der die namhaften Forschergruppen im Bereich der Software-Verifikation ihre neusten Ergebnisse in Verifikationswerkzeugen implementieren und zur vergleichenden Evaluierung einreichen.
Für den Wettbewerb werden Verifikationsprobleme aus vielen Bereichen der C-Programmierung gesammelt und für den Vergleich verwendet. Zur Zeit befinden sich in der Benchmark-Sammlung 9523 Verifikationsprobleme. Benutzer können sich dann die besten Werkzeuge der für sie passenden Kategorie aussuchen.
Im Vortrag werden die Regeln, die Durchführung auf einem Rechencluster an der LMU und die Ergebnisse des Wettbewerbs präsentiert.
Website zur Competition: https://sv-comp.sosy-lab.org/
Referent*innen
Prof. Dr. Dirk Beyer
LMU, Software and Computational Systems Lab at LMU Munich
https://www.sosy-lab.org/
Dirk Beyer is Full Professor of Computer Science and has a Research Chair for Software and Computational Systems 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 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.
Web: https://www.sosy-lab.org/people/beyer/