VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.

263-2812-00L 5 Credits MSC , WBZ D-INFK

Program Verification

Lecturers & Examiners: Dr. Malte Schwerhoff, Dr. Marco Eilers
VVZ CR 3.13

Last Updated: 2026-06-03 00:14:09

Abstract

A hands-on introduction to the theory and construction of deductive program verifiers, covering both powerful techniques for formal program reasoning, and a perspective over the tool stack making up modern verification tools.

Objective

Students will earn the necessary skills for designing, developing, and applying deductive verification tools that enable the modular verification of complex software, including features challenging for reasoning such as heap-based mutable data and concurrency. Students will learn both a variety of fundamental reasoning principles, and how these reasoning ideas can be made practical via automatic tools. By the end of the course, students should have a good working understanding and decisions involved with designing and building practical verification tools, including the underlying theory. They will also be able to apply such tools to develop formally-verified programs.

Content

The course will cover verification techniques and ways to automate them by introducing a verifier for a small core language and then progressively enriching the language with advanced features such as a mutable heap and concurrency. For each language extension, the course will explain the necessary reasoning principles, specification techniques, and tool support. In particular, it will introduce SMT solvers to prove logical formulas, intermediate verification languages to encode verification problems, and source code verifiers to handle feature-rich languages. The course will intermix technical content with hands-on experience.

Resources

Lecture Notes

The slides will be available online.

Literature

Will be announced in the lecture.

Learning Materials (Links)

General Information

Language
English
Levels
MSC , WBZ
Frequency
Yearly recurring

Examination

Type
graded semester performance
The grade for the course is determined by a midterm and a project presentation. The weight of each component will be announced at the beginning of the course.Last cancellation/deregistration date for this graded semester performance: end of week 3 of the semester. Please note that after that date, no deregistration will be accepted and a "no show" will appear on your transcript.

Registration & Places

Max Places
40
Priority: Registration for the course unit is only possible for the primary target group

Course Components

Type Title Time & Place Hours
lecture with exercise Program Verification
  • Wed 09:15-12:00 (CAB G 56)
3 h weekly
independent project Program Verification No time listed 1 h weekly

Offered In