Information Security Group

Search

EN

Formal Methods and Functional Programming

Spring Semester 2026, Bachelor course (252-0058-00)

Overview

Lecturers: Prof. Dr. David Basin, Prof. Dr. Ralf Jung, Prof. Dr. Michalis Kokologiannakis

Classes: Tuesdays 10-12 and Thursdays 10-12

Credits: 7 ECTS (4V + 2U)

Language: English (lectures), English and German (exercises)

Exercise classes: Tuesdays 14-16, Tuesdays 16-18, Wednesdays 8-10, or Wednesdays 16-18

For questions/issues concerned with the first half (Functional Programming), please contact Matthias Brun; for the second half (Formal Methods), please contact Johannes Hostert.

Announcements

  • [2026.02.05] The course webpage for this year's FMFP is up and running!
  • [2026.04.14] The FM team has taken over the website from the FP team.
  • [2026.04.17] The lecture livestream to HG E 3 has been terminated due to low demand. Please come to HG E 7 from now on.
  • [2026.04.30] The exercise session on Wednesdays 8:15 with Yushuo Xiao in ETZ F 91 is now cancelled. Please instead attend Anqi Li's session, happening at the same time in CAB G 52.
  • [2026.04.30] The exercise session on Wednesdays 16:15 with João Carlos Mendes Pereira in CHN F 46 is now cancelled. Please instead attend Yuchen Gu's session, happening at the same time in CHN D 42.
  • [2026.07.28] We want to make the following clarification on exam-relevance: While protocol modeling is exam-relevant, the exact Promela syntax is not. E.g. it is not exam-relevant to know where precisely semicolons are needed or how the if/do syntax works. The same is true for Viper syntax.
  • [2026.07.28] In the final exam, you will be provided an appendix which protected page you can already download now. Note that this appendix only contains definitions from the FM part, for FP, some of the relevant definitions and rules will be included directly in the tasks, similar to past years.

Course material

Week 14

Week 13

Week 12

Week 11

Week 10

Week 9

Week 8

Week 7

Week 6

Week 5

Week 4

Week 3

Week 2

Week 1

General Information

Course material:

All the course material will be uploaded on this website.

For the first part of the course, we will also use CodeExpert for programming exercises.

Lectures:

The lecture will be held in HG E 7. If not all students fit into the room, there will be a live streaming of the lecture in HG E 3. Please come to HG E 7 first.

Attendance is strongly recommended. No recordings will be provided.

Exercise Sessions:

You can enroll here: https://expert.ethz.ch/enroll/SS26/fmfp.

Exam and Quizzes:

There will be a 180 minutes written examination. This examination covers both halves of the course. Note that the examination is only offered in the session after the course unit.

There will also be two graded midterm quizzes (FP: March 12; FM: May 12). Each quiz will be 30 minutes and each may improve the final grade.

 

Description

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 modelling and implementing systems.

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 analyse 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 modelled 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

Literature for the first part

Haskell links

The external page Zurich Haskell user group maintains a collection of external page Haskell links useful for both Haskell beginners and experts.

Proof checker

The proof checker CYP for induction proofs is external page available on GitHub.

Literature for the second part

Additional literature for interested students

  • Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998.
  • Harold Abelson and Gerald Jay Sussman with Julie Sussman. Structure and Interpretation of Computer Programs. MIT Press, 1996. (external page full version online)
JavaScript has been disabled in your browser