Kooperative Softwareverifikation

• Antragstellerinnen / Antragsteller: Professor Dr. Dirk Beyer; Professorin Dr. Heike Wehrheim
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen
• Förderung: Förderung seit 2019
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 418257054

Softwareverifikation zielt auf die Sicherung hoher Qualität von Software, insbesondere auf den Nachweis der Abwesenheit von unbeabsichtigtem oder fehlerhaftem Verhalten. Heutzutage gibt es eine Reihe von Werkzeugen für Softwareanalysen, die unterschiedliche Technologien zur Verifikation nutzen, angefangen von dynamischen über statische Analysen bis hin zum Model-Checking. Diese Techniken haben alle verschiedene Stärken und Schwächen. Das Ziel dieses Projektes ist die Erhöhung von Präzision und Performance von Softwareverifikation durch die Kooperation von verschiedenen Werkzeugen und Techniken. Kooperative Softwareverifikation benötigt (1) Möglichkeiten zum Austausch von Informationen zwischen Verifikationstools und die korrekte Nutzung dieser Informationen, und (2) Verfahren zum Lernen der zweckmäßigsten Art und Weise der Kooperation. Kooperation zielt dabei auf das Aufteilen von Verifikationsaufgaben auf Werkzeuge, sodass jedes Werkzeug die Aufgaben erledigt, für die es am besten geeignet ist. Kooperation zielt aber auch darauf, das Vertrauen in die Gültigkeit von Verifikationsergebnissen zu erhöhen, zum Beispiel indem ein Werkzeug das Ergebnis eines anderen überprüft. Die Zielsetzung des Projektes ist daher die Entwicklung einer praktischen Methodik der kooperativen Softwareverifikation, basierend auf einer präzisen formalen Theorie der Kooperation. Untersucht werden sollen dabei Sicherheitseigenschaften (Safety) von Software.

• DFG-Verfahren: Sachbeihilfen