Thema: Aktives Lernen für Invarianten

Thema: Aktives Lernen für Invarianten

Grunddaten

Titel Aktives Lernen für Invarianten
Beschreibung

Aktives Lernen für Invarianten

Motivation

Das Finden von korrekten und hilfreichen Invarianten ist eine der Kernaufgaben bei der Softwareverifikation. In den letzten Jahren wurden verschiedene Ansätze zur Invarianten-Generierung vorgestellt, die verschiedene Machine Learning Techniken verwenden, darunter von Li et al. [1], die in Ihrer Arbeit einen aktiven Lernalgorithmus auf Basis einer Support-Vektor Maschine verwenden.  Um die verschiedenen Ansätze vergleichen zu können, wurde das MIGML Framework entwickelt. In diesem Framework lassen sich verschiedenen Techniken abbilden und damit vergleichen. Allerdings ist das MIGML Framework aktuell nur in der Lage, passive Lernalgorithmen zu unterstützen. Daher kann der Ansatz von Li et al. Nicht abgebildet werden.

 

 

[1] Jiaying Li, Jun Sun, Li Li, Quang Loc Le, and Shang-Wei Lin. 2017. Automatic loop-invariant generation and refinement through selective sampling. In Proc. ASE 2017.

 

Heimateinrichtung Department für Informatik
Art der Arbeit praktisch / anwendungsbezogen
Abschlussarbeitstyp Bachelor
Autor Jan Frederik Haltermann, M. Sc.
Status verfügbar
Aufgabenstellung

Inhalt und Ziele

In dieser Arbeit soll das existierende MIGML Framework konzeptionell erweitert werden, um aktive Lernalgorithmen zu unterstützen, sodass der oben genannte Ansatz im Anschluss durch das MIGML Framework abgebildet werden können. Neben der Implementierung der konzeptionellen Erweiterung muss der in der Arbeit verwendete Lernalgorithmus implementiert werden, wobei für die Realisierung existierende Komponenten von MIGML wiederverwendet werden können.
Im Anschluss soll in einer umfangreichen Evaluation die Performance des neuen Ansatzes  (1) mit den existierenden Ansätzen in MIGML und (2) anderen Tools zur Invariantengenrierung / Verifikation verglichen werden.

Voraussetzung

Grundlegende Programmiererfahrung mit Java

Erstellt 02.11.2021