|
Automatisierte Programmverifikation
(V4 + Ü2, SS 2003)
|
|
Ankündigung (30. 9. 2003)
Das Skript zur Vorlesung ist mittlerweile fertig überarbeitet und kann
im
Sekretariat des Lehr- und Forschungsgebiets Informatik II zum Kopieren
ausgeliehen werden.
Inhalt
Um die Zuverlässigkeit und Korrektheit von Programmen zu garantieren,
reicht es nicht aus, 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.
Contents
In order to guarantee the reliability and correctness of
programs, testing is not sufficient. Instead, a formal verification
of programs is required.
However, in general such verification proofs can be very costly and
time-consuming. In particular, this holds for large programs used in
practice.
Therefore, the goal is to mechanize program verification
as much as possible. For that purpose one has to use proof
tools which can verify correctness statements about programs
automatically.
Thus, the course focuses on techniques to automate the task of program
verification. The essential proof technique required
to handle programs with loops or recursion is
induction. Hence, we will introduce techniques to
mechanize induction proofs for the verification of
programs in a simple functional language. Moreover, we
will also present methods to prove the termination of
programs automatically.
Sprache
deutsch
Literatur
- C. Walther: Mathematical Induction. In "Handbook of Logic in Artificial Intelligence and Logic Programming", Vol. 2, D.M. Gabbay, C.J. Hogger,
J.A. Robinson (eds.), Oxford University Press, pages 127-227, 1994.
- T. Arts and J. Giesl:
Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science, 236:133-178, 2000.
- A. Bundy: The Automation of Proof by Mathematical Induction. In "Handbook of Automated Reasoning", J.A. Robinson, A. Voronkov (ed.), Elsevier & MIT Press,
pages 845-911, 2001.
- K.H. Bläsius & H.-J. Bürckert: Deduktionssysteme. Oldenbourg Verlag, 1992.
Zuordnung
Theoretische Informatik, Informatik Vertiefung
Scheinbedingungen
Um einen Übungsschein zu erhalten, müssen Sie
50% der Punkte in den Übungen erreichen
und eine kleine mündliche Prüfung bei D. Dlugosz am Ende des
Semesters bestehen. Den Erwerb eines Übungsscheins empfehlen wir sehr, da
dies eine gute Vorbereitung für die Diplomprüfung darstellt.
Übungen
Die Übungensblätter werden in der Regel dienstags in der Vorlesung
ausgegeben und können
bis zum Mittwoch der darauf folgenden Woche (8 Tage später) abgegeben werden.
Darüber hinaus sind die Übungsblätter auch auf dieser Webseite erhältlich.
Die Bearbeitung der Aufgaben sowie die Abgabe sollte möglichst in Zweiergruppen
erfolgen.
- Übung 1 (2. Mai 2003)
ps,
pdf
- Übung 2 (6. Mai 2003)
ps,
pdf
- Übung 3 (13. Mai 2003)
ps,
pdf
- Übung 4 (20. Mai 2003)
ps,
pdf
- Übung 5 (27. Mai 2003)
ps,
pdf
- Übung 6 (3. Juni 2003)
ps,
pdf
- Übung 7 (17. Juni 2003)
ps,
pdf
; Lösung (ps),
(pdf)
- Übung 8 (24. Juni 2003)
ps,
pdf
- Übung 9 (1. Juli 2003)
ps,
pdf
- Übung 10 (8. Juli 2003)
ps,
pdf
- Übung 11 (15. Juli 2003)
ps,
pdf
- Übung 12 (22. Juli 2003)
ps,
pdf
Folien
Hier sind die in der Vorlesung verwendeten Folien.
- Folie 1 (2. Mai 2003)
ps,
pdf
- Folie 2 (9. Mai 2003)
ps,
pdf
- Folie 3 (13. Mai 2003)
ps,
pdf
- Folie 4 (20. Mai 2003)
ps,
pdf
- Folie 5 (27. Mai 2003)
ps,
pdf
- Folie 6 (30. Mai 2003)
ps,
pdf
- Folie 7 (6. Juni 2003)
ps,
pdf
- Folie 8 (17. Juni 2003)
ps,
pdf
- Folie 9 (20. Juni 2003)
ps,
pdf
- Folie 10 (24. Juni 2003)
ps,
pdf
- Folie 11 (27. Juni 2003)
ps,
pdf
- Folie 12 (1. Juli 2003)
ps,
pdf
- Folie 13 (4. Juli 2003)
ps,
pdf
- Folie 14 (8. Juli 2003)
ps,
pdf
- Folie 15 (11. Juli 2003)
ps,
pdf
- Folie 16 (18. Juli 2003)
ps,
pdf
- Folie 17 (22. Juli 2003)
ps,
pdf
- Folie 18 (22. Juli 2003)
ps,
pdf
- Folie 19 (25. Juli 2003)
ps,
pdf
- Folie 20 (29. Juli 2003)
ps,
pdf
