Bachelor Program - Program Verification
VO3 + PS2 SS 2026 703083 + 703084
Introduction
The lecture covers the following topics:
- validation and verification
- partial correctness and termination
- automatic termination analysis
- usage of SMT-solvers
- specification of properties of programs
- verification of functional programs
- verification of imperative programs
- proof techniques: induction, invariants, generalization
Language
German
Prerequisites
Knowledge about functional programming and logic.
Lecturer
| Type | Lecturer | Room | Consulting Hours |
| VO+PS | René Thiemann | 3M09 | Tuesday 10:15 – 11:15 |
Slides
The slides will be made avaiable during the semester.
| Topics | Slides | Sources |
| Part 1: Introduction | PDF (x4) | |
| Part 2: A Logic for Program Specifications | PDF (x4) | |
| Part 3: Semantics of Functional Programs | PDF (x4) | |
| Part 4: Checking Well-Definedness of Functional Programs | PDF (x4) | |
| Part 5: Reasoning about Functional Programs | PDF (x4) | Demo.txt (rename file to demo.thy) |
| Part 6: Verification of Imperative Programs | ||
| Part 7: Certification | ||
| Part 8: Summary and Outlook |
Evaluation
A past exam will be reviewed in class on June 15 for practice purposes.
The 1st exam will take place on June 22 (closed book).
A 2nd and 3rd exam will be offered in September and January, if necessary.
Proseminar
A new worksheet is posted here every week. Completed assignments must be marked in OLAT. The deadline is 5:00 p.m (17:00). on the Monday before the proseminar. Solutions will be made available in OLAT.
| Week | Date | Exercises | Material |
| 01 | 10.03 | ||
| 02 | 17.03 | template_02.txt (rename file to "template_02.hs") | |
| 03 | 24.03 | ||
| 04 | 14.04 | template_04.txt (rename file to "template_02.hs") | |
| 05 | 21.04 | template_05.txt (rename file to "template_02.hs") | |
| 06 | 05.05 | ||
| 07 | 12.05 | ||
| 08 | 19.05 | ||
| 09 | 26.05 | ||
| 10 | 02.06 | ||
| 11 | 09.06 |
Grading
Grades for the introductory seminar are calculated as follows.
- Let WP be the percentage of points earned from the weekly assignments
- Let TP be the percentage for your performance at the blackboard
- Calculate P = 0.8 * WP + 0.2 * TP as the weighted percentage
- If P is at least 50% (62.5%, 75%, 87.5%), then you receive a passing grade of 4 (3, 2, 1)