Motivation:
Im Jahr 2018 haben Boerding et al. das neue Konzept der Inter-Method Contracts für Java vorgeschlagen, welches das präzise Ausdrücken von Abhängigkeiten zwischen Methoden ermöglicht [1]. Sie stellten mit JMC eine Sprache zum Spezifizieren und mit JMCTest ein Tool zum dynamischen überprüfen der Inter-Method-Contracts von Javaprogrammen vor. JMCTest generiert vollkommen automatisch Objekte, auf denen die Methoden ausgeführt werden und die Validität der Contracts überprüft wird. Mit JMCTest konnten sie die Verletzung von Standard Inter-Method-Contracts in großen Projekten (z.B. JBoss, Java RT) nachweisen. Im Vergleich mit anderen Verifikationstools, die (manche) Inter-Method-Contracts prüfen, konnten Bugs gefunden werden, die von den anderen Tools nicht gefunden wurden.Obwohl JMCTest Contract-Verletzungen gefunden hat, ist es momentan noch ein akademischer Prototyp. Deshalb lässt sich das Tool an mehreren Stellen optimieren: Neben der Erweiterung des Funktionsumfangs, sodass z.B. Generics und innere Klassen unterstützt werden, kann der Algorithmus zur Erstellung und Modifikation der Eingaben der Test-Engine optimiert werden.

Ziele & Inhalt der Arbeit:
Ziel der Arbeit ist die Optimierung der Performance von JMCTest, um weitere Contract-Verletzungen zu finden. Deshalb sollen weitere Java-Features unterstützt werden. Das Tool soll in der Lage sein, Klassen zu analysieren, die Generics und innere Klassen enthalten und solche, die nicht über einen öffentlichen Konstruktor verfügen (z.B. mit dem Factory-Pattern). Darüber hinaus soll das Set der Elemente, die zur Generierung von Testdaten verwendet werden, erweitert werden. Momentan werden lediglich primitive Datentypen und Objekte zur Erstellung von Testdaten verwendet. Daher sollen komplexere Java-Konstrukte wie Arrays, Listen Maps und Enumerations unterstützt werden.  Darüber hinaus soll mindestens eine Strategie zur Modifizierung von Testdaten ausgearbeitet und implementiert werden. Solch eine Strategie kann zum Beispiel das zufällige Aufrufen von Methoden enthalten. Um besseres Feedback zu den gefundenen Verletzungen zu bieten, soll der Export der der Testfälle, die die Verletzung enthalten, verbessert werden.
Im Anschluss sollen die entwickelten Techniken evaluiert werden und mit potenziell mit ähnlichen Tools verglichen werden. Im Vergleich soll gezeigt werden, dass die Erweiterungen zu besseren Resultaten (mehr gefunden Fehlern) führen.Neben dem Contract „EqualsImpliesHashcode“ kann es noch weitere Contracts geben, die grundlegend in Java enthalten sind, z.B. für Datenstrukturen wie Arrays oder Listen. Wenn im Rahmen der Arbeite weitere Contracts identifiziert werden, soll die Performance von JMCTest mit ähnlichen Tools verglichen werden.

Literatur:
[1] Börding P., Haltermann J., Jakobs MC., Wehrheim H. (2018) JMCTest: Automatically Testing Inter-Method Contracts in Java. In: Medina-Bulo I., Merayo M., Hierons R. (eds) Testing Software and Systems. ICTSS 2018. Lecture Notes in Computer Science, vol 11146. Springer, Cham

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