Large Language Models (und insbesondere ChatGPT) werden immer effektiver darin, Programmcode zu generieren.
Leider ist jedoch die Code Generierung nicht immer fehlerfrei, was zu Bugs oder Sicherheitslücken im Code führen kann.
Insbesondere in sicherheitskritischen Systemen kann dies schwerwiegende Folgen haben. 

Die meisten existierenden Ansätze versuchen dies zu verhindern, indem sie Tests für den generierten Code entwickeln
oder entwickeln lassen (durch ein weiteres Language Model). Testen kann aber nur Fehler aufdecken, aber nicht 
zeigen, dass Code fehlerfrei ist. Aus diesen Grund wollen wir in dieser Bachelorarbeit
den ersten Schritt wagen, um zu evaluieren, ob man Formale Verifikation einsetzen kann, 
um die Resultate der Code Generierung zu verifizieren.

Die Idee ist es, automatisch formale Spezifikationen für ein Generierungsproblem zu erzeugen
und diese dann mit Hilfe eines formalen Verifikationswerkzeug zu überprüfen.
Typischerweise bestehen Generierungsprobleme aus eine natürlichsprachlichen Beschreibung
zusammen mit einer Menge von Tests. Das Large Language Model generiert dann Code, welcher
der Beschreibung entsprechen soll.

Das Ziel der Bachelorarbeit ist ein Ansatz zu entwickeln, um mit ChatGPT formale Spezifikationen
basierend auf der natürlichsprachlichen Beschreibung (und den Tests) zu generieren. Die Bachelorarbeit
fokussiert sich auf Generierungsprobleme in C und wir verwenden State-of-the-Art Verifikationswerkzeuge, um die generierten Spezifikation zu evaluieren.

Die Bachelorarbeit kann sowohl in Englisch als auch Deutsch verfasst werden. Gute Englischkenntnisse
sind dennoch ein Muss zur Interaktion mit ChatGPT. Gute Programmierkenntnisse in Python (für die Toolentwicklung) und/oder in C wären vom Vorteil.