VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.
Formalizing Analysis of Algorithms
Last Updated: 2026-06-01 11:30:47
Abstract
In this course, participants will learn about formal methods for proving mathematical properties of algorithms, including their correctness and running time. The first part of the course introduces Lean 4, an interactive theorem prover, and their foundational principles.The second part applies these tools to the formal analysis of a variety of algorithms.
Objective
Participants will learn new techniques for writing formal proofs about algorithms and will be able to use interactive theorem provers to verify algorithm correctness and analyze their runtime.
Content
The first part of the course introduces interactive theorem provers and their use in formalizing hand-written mathematical proofs. Participants will learn essential proof techniques, including basic tactics, recursion, and induction principles. The course will also cover how to work with inductive types, providing a foundation for expressing and reasoning about mathematical structures formally. In the second part of the course, the focus shifts to the formal verification of algorithms. Students will learn to specify algorithms using functional programming and use theorem provers to formally verify their correctness and analyze their runtime. This section includes the formalization of basic algorithmic paradigms such as divide-and-conquer and greedy algorithms.
General Information
- Language
- English
- Levels
- MSC , WBZ
Examination
- Type
- graded semester performance
Registration & Places
- Max Places
- 30
Course Components
| Type | Title | Time & Place | Hours |
|---|---|---|---|
| lecture with exercise | Formalizing Analysis of Algorithms |
|
2 h weekly |
| independent project | Formalizing Analysis of Algorithms | No time listed | 1 h weekly |