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

252-0058-00L 7 Credits BSC D-INFK
You're viewing possible stale or outdated data. Please check the latest semester for more up-to-date information.

Formal Methods and Functional Programming

Lecturers & Examiners: Prof. Dr. David Basin, Prof. Dr. Peter Müller, Prof. Dr. Ralf Jung
VVZ CR 3.52

Last Updated: 2026-06-01 11:33:38

Abstract

In this course, participants will learn about new ways of specifying, reasoning about, and developing programs and computer systems. The first half will focus on using functional programs to express and reason about computation. The second half presents methods for developing and verifying programs represented as discrete transition systems.

Objective

In this course, participants will learn about new ways of specifying, reasoning about, and developing programs and computer systems. Our objective is to help students raise their level of abstraction in modeling and implementing systems.

Content

The first part of the course will focus on designing and reasoning about functional programs. Functional programs are mathematical expressions that are evaluated and reasoned about much like ordinary mathematical functions. As a result, these expressions are simple to analyze and compose to implement large-scale programs. We will cover the mathematical foundations of functional programming, the lambda calculus, as well as higher-order programming, typing, and proofs of correctness. The second part of the course will focus on deductive and algorithmic validation of programs modeled as transition systems. As an example of deductive verification, students will learn how to formalize the semantics of imperative programming languages and how to use a formal semantics to prove properties of languages and programs. As an example of algorithmic validation, the course will introduce model checking and apply it to programs and program designs.

Resources

Learning Materials (Links)

General Information

Language
English
Levels
BSC
Frequency
Yearly recurring

Examination

Type
session examination
Mode
written 180 minutes
Aids
None
We offer 2 graded midterms, in the first and second half. Each midterm will be 30 minutes and act as a bonus, that is, may improve the grade, but will not make it worse. In the positive case, each midterm will count 10% of the total grade.

Course Components

Type Title Time & Place Hours
lecture Formal Methods and Functional Programming
Findet im HG E 7 mit Videoübertragung ins HG E 3 statt. Am 27. Februar 2025 ausnahmsweise im HG E 7 mit Videoübertragung ins HG F 7.
  • Tue 10:15-12:00 (HG E 3)
  • Tue 10:15-12:00 (HG E 7)
  • Thu 10:15-12:00 (HG E 3)
  • Thu 10:15-12:00 (HG E 7)
  • 27.02 Date 10:15-12:00 (HG F 7)
  • 13.05 Date 09:15-11:00 (HG E 23)
4 h weekly
exercise Formal Methods and Functional Programming
  • Tue 14:15-16:00 (CAB G 52)
  • Tue 16:15-18:00 (ETZ F 91)
  • Tue 16:15-18:00 (ETZ G 91)
  • Wed 08:15-10:00 (CAB G 52)
  • Wed 08:15-10:00 (ETZ F 91)
  • Wed 08:15-10:00 (HG E 33.5)
  • Wed 08:15-10:00 (LEE C 114)
  • Wed 16:15-18:00 (CHN D 42)
  • Wed 16:15-18:00 (CHN F 46)
  • Wed 16:15-18:00 (HG G 26.5)
  • 28.05 Date 08:15-10:00 (LEE D 105)
2 h weekly

Offered In