In diesem Seminar für Masterstudierende werden wir uns mit dem Thema der Invariantengenerierung in der Programmverifikation beschäftigen. Invarianten beschreiben Programmeigenschaften (Aussagen über die Werte von Programmvariablen), die immer gelten (also invariant sind). "Immer" kann sich hierbei auf das gesamte Programm oder auf eine Schleife in einem Programm beziehen. Die Techniken, die wir kennenlernen, nutzen logisches Schließen, Induktion oder auch Techniken des maschinellen Lernens.