Motivation:
Um die Korrektheit von Software zu analysieren, ist das Generieren von starken Invarianten eine entscheidende Aufgabe. Eine starke Invariante wird oftmals als Witness im Beweis der Korrektheit von Software verwendet. Daher ist dieser Bereich aktuell in der Forschung relvant. Im Jahr 2018 haben Zhu et al. einen Ansatz zum Lernen von Invarianten für Programme mit Schleifen entwickelt [1]. Zuerst werden dafür Testdaten generiert. Hierfür werden mögliche Werte der Schleifenvariablen während der Programmausführung generiert und klassifiziert, ob die Werte während einer Programausführung beobachtbar sind. Dafür wurden Constrained Horn Clauses verwendet. Im Anschluss wurde eine Support Vector Maschine (SVM) auf den generierten Daten trainiert. Das von der SVM gelernt Model stellt eine mögliche Programminvariante dar, die mit Hilfe von Decision Trees vereinfacht wurde.

Ziele und Umfang:
Während der Arbeit soll die vorgestellte Idee mit einem anderen ML Ansatz evaluiert werden. Dafür muss der Ansatz zuerst implementiert werden, wobei decision trees zum lernen von Invarianten verwendet werden sollen. Anstelle von Constrained Horn Clauses sollen zur Datengenerierung und zum Erzeugen von überapproximativen Gegenbeispielen Symbolic Execution verwendet werden. Diese Gegenbeispiele werden analysiert, um Testdaten zu generieren. Anschließend soll der neu entwickelte Approach mit dem ursprünglichen verglichen werden. Außerdem muss evaluiert werden, ob das Ersetzten der SVM durch anderen Verfahren (wie logistic regression) im Originalansatz zu besseren Resultaten führt. Die Implenentierung soll im CPAchecker [2] Framework erfolgen, wobei existierenden ML Bibliotheken verwendet werden sollen.

Literatur:
[1] Zhu, He, Stephen Magill, and Suresh Jagannathan. "A data-driven CHC solver." ACM SIGPLAN Notices. Vol. 53. No. 4. ACM, 2018.
[2] cpachecker.sosy-lab.org