Seminar
Fortgeschrittene Techniken der Softwareverifikation (FTSV)

In diesem Seminar befassen Sie sich mit Themen zu den aktuellen Forschungsinhalten der Arbeitsgruppe Semantik und Verifikation paralleler System. Es werden sowohl klassische als auch aktuelle Forschungsarbeiten im Bereich Softwareverifikation (d.h. Model Checking, Programmanalyse, Testen, etc.) behandelt. Die Themen des aktuellen Seminars finden Sie weiter unten auf der Seite.

Seminar: Fortgeschrittene Techniken der Softwareverifikation (FTSV)

Das Seminar wird nicht mehr länger angeboten. In diesem Seminar befassten wir uns mit Themen zu den aktuellen Forschungsinhalten der Arbeitsgruppe Semantik und Verifikation paralleler System. Es werden sowohl klassische als auch aktuelle Forschungsarbeiten im Bereich Softwareverifikation (d.h. Model Checking, Programmanalyse, Testen, etc.) behandelt.

Lerninhalte- und Ziele

Während des Seminars werden Sie unter Anleitung

  • sich auf Basis von vorgegebener und selbst gefundener, wissenschaftlicher Literatur in Ihr Thema einarbeiten
  • einen Vortrag über Ihr Thema vorbereiten und vor den anderen Teilnehmern halten, um mit ihnen anschließend über Ihr Thema zu diskutieren,
  • eine wissenschaftliche Ausarbeitung verfassen, die einen zusammenfassenden Überblick über Ihr Thema gibt.

Nach erfolgreichem Abschluss des Seminars können sich die Studierenden anhand von Ausgangsliteratur eigenständig in ein wissenschaftliches Thema einarbeiten und dieses Thema einem heterogenen Fachpublikum sowohl mündlich als auch schriftlich präsentieren.

Im Detail können die Studierenden Methoden zur Literaturrecherche anwenden und die Relevanz von gefundener Literatur beurteilen. Sie können den wesentlichen Inhalt einer wissenschaftlichen Veröffentlichung ermitteln und diesen kritisch beurteilen. Außerdem sind sie in der Lage verschiedene wissenschaftliche Arbeiten miteinander zu vergleichen. In einem mündlichen Vortrag können die Studierenden ihr Thema und ihre Ergebnisse einem heterogenen Fachpublikum erklären und ihre Ergebnisse vor diesem Publikum verteidigen. Zusätzlich können die Studierenden in einer schriftlichen Ausarbeitung ihr Thema und ihre Ergebnisse beschreiben.

Vorkenntnisse

Empfohlen. Informatik- und Mathematikkenntnisse entsprechend den ersten 4 Semestern des Bachelorstudiengangs Informatik

Hilfreich. Besuch einer Veranstaltung des Fachgebietes Semantik und Verifikation paralleler Systeme

Seminarthemen vergangener Semester

In diesem Seminar beschäftigen wir uns mit Spezifikationssprachen und Zwischensprachen für die Verifikation. Spezifikationssprachen erlauben es Anforderungen, Annahmen und Garantien bezüglich funktionalen Verhaltens, etc. zu spezifizieren und mittels Verifikation zu prüfen. Zwischensprachen erlauben es einem Programme in verschiedenen Programmiersprachen mit dem gleichen Verifizierer zu analysieren. Gleichzeitig sind Zwischensprachen häufig darauf ausgelegt, die Verifikation zu vereinfachen, z.B. implizites Verhalten explizit zu machen, möglichst wenig Konstrukte zu verwenden ohne die Ausdrucksstärke zu verlieren, usw.

Zwischensprachen

Spezifikationssprachen

Zwischensprachen mit Spezifikationsanteil

In diesem Seminar werden wir uns Werkzeuge zur Analyse und Verifikation von Softwareprogrammen widmen. Die Werkzeuge, die wir uns anschauen werden, unterscheiden sich in den Techniken und unterstützten Programmiersprachen. Im Detail werden wir uns die folgenden Werkzeugen anschauen.

Frameworks für Java Analyse

Frameworks für C Analyse

Verifizierer für C Programme

Verifizierer für Boogie Programme

Diese Seminar behandelt Themen aus dem Bereich automatischer Testfallgenerierung. Das Ziel der Testfallgenerierung ist es Testeingaben zu erzeugen, die Fehler in Programmen entdecken, oder eine Menge von Testeingaben zu erzeugen, die zusammen ein gewisses Überdeckungskriterium erreichen. Konkrekt beschäftigen wir uns in diesem Seminar mit Werkzeugen zur automatischen Testgenerierung, die ihre Testeingaben (1) zufallsbasiert, (2) mit such-basierten Ansätzen, (3) mit Hilfe von symbolischer Ausführung oder (4) mit Hilfe von Erreichbarkeitsanalysen generieren.

Random Test Generation

Search-based Test Generation

Test Generation with Symbolic Execution

Test Generation with Reachability Analyses

Diese Seminar behandelt Themen unseres Forschungsbereichs Überprüfung von Verifikationsergebnissen. Das Ziel der Prüfung ist es, das Vertrauen in das Verifikationsergebnis zu stärken. So kann man z.B. prüfen, ob die Verifikation tatsächlich durchgeführt wurde und ob das Verifikationswerkzeug fehlerfrei gearbeitet hat. In diesem Seminar beschäftigen wir uns mit (1) verschiedenen Protokollen der Prüfung, mit (2) Prüftechniken für Datenflussanalysen, abstrakter Interpretation, oder Model Checking.

Prüfprotokolle

Prüftechniken für Model Checking

  • Temporal Safety Proofs
    Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, George C. Necula, Grégoire Sutre, Westley Weimer: Temporal-Safety Proofs for Systems Code, CAV 2002.
  • Extreme Model Checking
    Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Marco A. A. Sanvido: Extreme Model Checking, Verification: Theory and Practice 2003.

Prüftechniken für Datenflussanalysen und abstrakte Interpretation

Diese Seminar behandelt Themen unseres Forschungsbereichs Kombination von Verifikationsverfahren. Insbesondere beschäftigen wir uns mit kooperativen Verifikationsverfahren. Das Ziel kooperativer Verifikationsverfahren ist die verschiedenen Stärken und Schwächen der Verifikationsverfahren zu nutzen und mächtigere Verfahren mittels Kooperation zu erreichen. In diesem Seminar beschäftigen wir uns mit drei Arten von Kooperationen (1) Bestätigung von Alarmen, (2) Aufteilung des Verifikationsaufwands und (3) algorithmische Integration von verschiedenen Verifikationsansätzen.

Ziel der Bestätigung von Alarmen ist die Anzahl der falschen Alarme zu reduzieren und den Entwicklern nur Alarme zu zeigen, die tatsächlich mit einen Testfall bestätigt und nachvollzogen werden können.

Bei der Aufteilung des Verifikationsaufwands werden verschiedene Teilaspekte oder verschiedene Teile des Programms von unterschiedlichen Verfahren geprüft. Häufig werden sequentielle Kombinationen genutzt, in denen das zweite Verifikationswerkzeug lediglich die übrig gebliebenen Beweisverpflichtungen prüfen muss.

In der algorithmische Integration von verschiedenen Verifikationsansätzen werden neue Verifikationsalgorithmen entwickelt die existierende Ansätze als Teilkomponenten nutzen.

Bestätigung von Alarmen

Aufteilung des Verifikationsaufwands

Algorithmische Integration von verschiedenen Verifikationsansätzen

Das Seminar ist aufgrund fehlender Teilnehmer ausgefallen und wird daher im folgenden Semester mit den gleichen Themen wieder angeboten.

Diese Seminar behandelt Themen unseres Forschungsbereichs inkrementelle Verifikation. Techniken der inkrementellen Verifikation sind eine Schlüsseltechnologie, um formale Verifikation in agilen Softwareprojekten einzusetzen. Um mit den vielen, schnellen Änderungen mithalten zu können. Umfasst inkrementelle Verifikation Techniken, die eine erneute Verifikation nach einer Programmänderung effizienter machen. Dafür nutzt inkrementelle Verifikation Informationen aus einer vorherigen Verifikation. Die Art der Information und ihrer Nutzung unterscheidet sich. Im Seminar betrachten wir vier Klassen von inkrementeller Verifikation: funktionale Äquivalenzprüfung, Nutzung von Zwischenergebnissen, Beweisadaption, und Beschränkung der Verifikation auf modifizierte Ausführungspfade.

Verfahren zu funktionalen Äquivalenzprüfung prüfen, ob modifizierte Programmteile (typischerweise Funktionen) das gleiche Ein- und Ausgabeverhalten zeigen wie der entsprechende Programmteil nach der Verifikation.

Verfahren, die Zwischenergebnisse wiederverwenden, vermeiden das Wiederentdecken von bereits bekannten Informationen, z.B. Invarianten, Antworten auf Erfüllbarkeitsanfragen, und Abstraktionsgrad. Ihre Annahme ist das viele dieser Informationen weiterhin gültig und benötigt werden.

In der Beweisadaption wird geprüft, welche Teile des Beweises weiterhin gültig sind. Gültige Beweisteile werden übernommen. Ungültige Beweisteile werden gelöscht und nur der die fehlenden Beweisteile wird durch erneute Verifikation wiederhergestellt.

Die letzte Klasse ist verwandt mit Beweisadaptionen. Verfahren, die sich auf modifizierte Pfade beschränken, stoppen die Verifikation von Pfaden sobald keine Veränderung mehr erreicht werden kann oder führen leichtgewichtige Verifikationsschritte aus solange noch keine Veränderung gesehen wurde.

Funktionale Äquivalenzprüfung

Wiederverwendung von Zwischenergebnissen

Beweisadaption

Überspringen von Verifikationsschritten