VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.
Computer-Aided Modelling and Reasoning
Last Updated: 2026-02-05 16:23:00
Abstract
The "computer-aided modelling and reasoning" lab is a hands-on course about using an interactive theorem prover to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The lab has two parts: The first introduces various modelling and proof techniques. The second part consists of a project in which the students apply these techniques
Objective
The students learn to effectively use a theorem prover to create unambiguous models and rigorously analyse them. They learn how to write precise and concise specifications, to exploit the theorem prover as a tool for checking and analysing such models and for taming their complexity, and to extract certified executable implementations from such specifications.
Content
The "computer-aided modelling and reasoning" lab is a hands-on course about using an interactive theorem prover to construct formal models of algorithms, protocols, and programming languages and to reason about their properties. The focus is on applying logical methods to concrete problems supported by a theorem prover. The course will demonstrate the challenges of formal rigor, but also the benefits of machine support in modelling, proving and validating. The lab will have two parts: The first part introduces basic and advanced modelling techniques (functional programs, inductive definitions, modules), the associated proof techniques (term rewriting, resolution, induction, proof automation), and compilation of the models to certified executable code. In the second part, the students work in teams of two on a project assignment in which they apply these techniques: they build a formal model and prove its desired properties. The project lies in the area of programming languages, model checking, or information security.
Resources
Literature
Textbook: Tobias Nipkow, Gerwin Klein. Concrete Semantics, part 1 ( www.concrete-semantics.org )
Learning Materials (Links)
- Main link
- Information
General Information
- Language
- English
- Levels
- MSC , WBZ
Examination
- Type
- ungraded semester performance
Registration & Places
- Max Places
- 40
Course Components
| Type | Title | Time & Place | Hours |
|---|---|---|---|
| practical/laboratory course | Computer-Aided Modelling and Reasoning |
|
7 h weekly |