Stud.IP Uni Oldenburg
University of Oldenburg
07.12.2022 05:22:45
ThesisTopics

Personal details

Title Aktives Lernen für Invarianten
Description

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.

 

Home institution Department of Computing Science
Type of work practical / application-focused
Type of thesis Bachelor's
Author Jan Frederik Haltermann, M. Sc.
Status available
Problem statement

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.

Requirement

Grundlegende Programmiererfahrung mit Java

Created 02/11/21