Bei Softwareverifikation geht es darum, zu zeigen, dass ein Programm, auf eine bestimmte Eigenschaft bezogen, korrekt ist oder einen Fehler enthält. Für diese Verifikationsaufgaben gibt es unterschiedliche Verifikationstools, wie zum Beispiel den CPAchecker, deren Leistung anhand von Benchmarks ermittelt wird. Häufig werden „function contracts“ zu Programmen hinzugefügt, die aus einer Vor- und Nachbedingung bestehen, um deren Verhalten formal zu spezifizieren und Programmeigenschaften zu dokumentieren.
In der BA sollen durch Eingaben in ein Programm, gemeinsam mit den entsprechenden Ausgaben, Testfälle generiert werden, aus denen durch einen Learner diese function contracts generiert werden. Bezüglich dieser Vor- und Nachbedingung sollen die dadurch annotierten Programme als korrekt verifiziert werden. Die Aufgaben der Abschlussarbeit bestehen darin, die Testfälle zu generieren, die function contracts zu lernen und deren Qualität zu überprüfen.