In dem dreijährigen DFG Projekt „Cooperative Software Verification“ wollen Prof. Dr. Heike Wehrheim und ihr Team zusammen mit Prof. Dr. Dirk Beyer und seinem Lehrstuhl der LMU München sowohl die Präzision als auch die Performance bereits bekannter Ansätze der Softwareverifikation verbessern. Dies ist insbesondere in sicherheitskritischen Bereichen notwendig, um die Sicherheit von Software zu garantieren. Erreicht werden soll diese Verbesserung durch die Kooperation verschiedener Werkzeuge.
Aufgabe der Softwareverifikation generell ist das Prüfen von Eigenschaften von Programmen. Ein erster Ansatz, Programme zu annotieren, um ihre Korrektheit zu folgern, wurde bereits 1949 von Alan Turing vorgeschlagen. Neben Verifikation nutzen Softwareentwickler Testverfahren, um das Verhalten ihrer Programme zu analysieren. In den letzten Jahren wurde in diesem Bereich ein enormer Fortschritt erzielt, auch wenn das Problem bekanntermaßen unentscheidbar ist. Heute gibt es eine Vielzahl von Ansätzen, die von dynamischer bis zu statischer Analyse reichen und alle besonderen Stärken und Schwächen haben.
Hier setzt das neue DFG Projekt mit Start am 01.10.2019 mit der kooperativen Softwareverifikation an. Benötigt für eine kooperative Analyse werden zum einen Möglichkeiten zum Austausch von Informationen zwischen Verifikationstools und die korrekte Nutzung dieser Informationen. Zum anderen sind Verfahren zum Lernen der zweckmäßigsten Art und Weise der Kooperation erforderlich. Letztendlich werden Verifikationsaufgaben auf Werkzeuge aufgeteilt, sodass jedes Werkzeug die Aufgaben erledigt, für die es am besten geeignet ist. Eine Kooperation soll aber auch das Vertrauen in die Gültigkeit von Verifikationsergebnissen erhöhen, zum Beispiel indem ein Werkzeug das Ergebnis eines anderen überprüft. Das Ziel des Projektes ist es, eine praktische Methodik der kooperativen Softwareverifikation und die dahinterliegende Theorie der Kooperation zu entwickeln.
In beiden Arbeitsgruppen gibt es bereits Vorarbeiten zur kooperativen Verifikation; die Idee zum Thema entstand daher unabhängig voneinander. Eine Zusammenarbeit bot sich aufgrund der komplementären Techniken der Arbeitsgruppen an und verspricht somit eine erfolgreiche Kooperation.
Weitere Informationen zum Projekt sind zu finden unter:
https://cs.uni-paderborn.de/sms/research/cooperative-software-verification/
