Die Programmverifikation beschäftigt sich damit, mittels formeller Beweise zu zeigen, dass ein bestimmtes Programm seine Spezifikation erfüllt. Dabei existieren verschiedene Verfahren, mit denen die Korrektheit eines Programms nachgewiesen oder widerlegt werden können. Ein Programmverifikationsverfahren ist die „Trace Abstraction“, bei welchem die Korrektheit eines Programms bewiesen oder widerlegt wird, indem mittels Abstrahierung gezeigt wird, dass die Fehlzustände eines Programmes unerreichbar sind beziehungsweise ein Beispiel für eine fehlerhafte Ausführung erzeugt wird. Dabei werden für ein Programm Interpolanten Automaten erzeugt, die unzulässige Programmausführungen akzeptieren. Sobald es für jede potenzielle Fehlausführung einen Interpolanten Automaten gibt, der diese Ausführung akzeptiert, ist bewiesen, dass alle Fehlzustände des Programms unerreichbar sind. Ziel der Masterarbeit ist eine Erweiterung des Verfahrens für Programme, die unter anderem auch Funktionsaufrufe tätigen. Dabei sollen Funktionen und Unterfunktionen auf eine rekursive Art und Weise abstrahiert werden. Dafür werden Funktionskontrakte berechnet und verwendet, die eine Approximation eines Funktionsaufrufes darstellen. Ist ein Kontrakt nicht ausreichend, um die Korrektheit des Programms zu beweisen, müssen aufgerufene Funktionen detaillierter betrachtet und gegebenenfalls strengere Kontrakte berechnet werden. Das Verfahren soll rekursiv auf weitere Unterfunktionen angewendet werden, bis ein Korrektheitsbeweis erbracht oder die Fehlerfreiheit des Programmes durch ein gefundenes Gegenbeispiel widerlegt werden kann. Ein solches Verfahren wird in dieser Masterarbeit ausgearbeitet, implementiert und evaluiert.