Um die Zuverlässigkeit und Korrektheit von Programmen zu garantieren, ist es
nicht hinreichend, sie nur zu testen, sondern es wird eine formale Verifikation
benötigt. Solche Verifikationsbeweise sind jedoch im allgemeinen sehr
aufwendig - insbesondere bei umfangreichen Programmen, wie sie in der Praxis
eingesetzt werden.
Aus diesem Grund wird versucht, die Aufgabe der Verifikation weitgehend automatisch
durchzuführen. Hierzu müssen automatische Beweissysteme verwendet werden,
die in der Lage sind, Korrektheitsaussagen über Programme nachzuweisen.
Das Ziel der Vorlesung ist daher die Vermittlung von Techniken zur Automatisierung
der Programmverifikation. Von zentraler Bedeutung ist hierbei das Beweisprinzip
der Induktion, das benötigt wird, um Eigenschaften von Programmen mit
Schleifen oder Rekursion zu verifizieren. Es wird gezeigt, wie solche
Induktionsbeweise zur Verifikation von Programmen in einer einfachen funktionalen
Programmiersprache automatisch durchgeführt werden können und es wird
darauf eingegangen, wie auch die Terminierung von Programmen automatisch gezeigt
werden kann.
Scheinbedingungen
Für den Übungsschein müssen 50% der Punkte in den Übungen erreicht
werden und voraussichtlich eine Klausur bzw. eine kleine mündliche Prüfung bestanden werden.
Den Erwerb eines Übungesscheines empfehlen wir sehr, da dies eine gute
Vorbereitung für die Diplomprüfung darstellt.
Übungen
Die Übungensblätter werden jeweils mittwochs in der Vorlesung
ausgegeben und können bis zum darauf folgenden Dienstag abgegeben werden.
