Funktionale Programmiersprachen wie etwa Haskell oder ML erlauben dem Programmierer, Prozeduren höherer Ordnung zu implementieren und zu verwenden. Eine Prozedur höherer Ordnung bekommt eine Funktion als Argument und wendet diese Funktion auf gewisse Werte an. Zum Beispiel wendet die Prozedur "map" eine Funktion auf alle Elemente einer Liste an und gibt die Liste der Ergebniswerte zurück. Der Nachweis, dass ein Programm höherer Ordnung eine gewisse Eigenschaft erfüllt, birgt besondere Herausforderungen, weil insbesondere auch indirekte Funktionsaufrufe zu betrachten sind: Der Aufruf "map(f, l)" enthält beispielsweise einen direkten Aufruf der Prozedur "map" und indirekte Aufrufe der Funktion "f", falls die Liste "l" nicht leer ist. Unter Verwendung einer Prozedur "g" höherer Ordnung kann eine Prozedur "f" durch so genannte Rekursion höherer Ordnung definiert werden. Dies bedeutet, dass die Prozedur "f" (direkt) die Prozedur "g" aufruft und sich selbst als Argument an "g" übergibt, was zu indirekten rekursiven Aufrufen führt. Diese indirekten rekursiven Aufrufe erschweren die Beweisführung über Programme höherer Ordnung. In dieser Dissertation zeigen wir, wie die Verifikation funktionaler Programme zweiter Ordnung durch halb-automatische Theorembeweiser unterstützt werden kann. Der Fokus auf Programme zweiter Ordnung bedeutet, dass eine Prozedur wie etwa "map" nur auf Funktionen erster Ordnung angewendet werden darf, nicht auf Funktionen höherer Ordnung. Dies genügt für die meisten in der Praxis auftretenden Beispiele und bietet Vorteile hinsichtlich der Semantik von Programmen. Unser Ziel ist der Nachweis der totalen Korrektheit von Programmen. Dies erfordert einen Beweis, dass das Programm terminiert und dass das Ergebnis der Berechnung eine vom Benutzer spezifizierte Eigenschaft erfüllt. Dementsprechend untersuchen wir zwei Hauptprobleme: Terminierungsanalyse und Theorembeweisen durch Induktion. Der allgemeine Beitrag dieser Dissertation ist die automatisierte Analyse der dynamischen Aufrufstruktur von Programmen zweiter Ordnung (verursacht durch indirekte Funktionsaufrufe). Insbesondere beschreiben wir eine Technik, die die Terminierung von zahlreichen in der Praxis auftretenden Prozeduren analysiert und beweist, sowie eine Technik, die automatisch Induktionsaxiome erzeugt, die zum Nachweis von Eigenschaften dieser Prozeduren mittels Induktion geeignet sind. Schließlich zeigen wir, wie die Beweise der Basis- und Schrittfälle durch einen automatisierten Theorembeweiser unterstützt werden können. Die vorgestellten Techniken wurden im Verifikationswerkzeug VeriFun implementiert. Mehrere Fallstudien zeigen, dass sich die Techniken in der Praxis bewähren und einen deutlich höheren Automatisierungsgrad bieten als andere induktive Theorembeweiser.