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 6 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, Dr. Jean-Raymond Abrial
VVZ CR 3.52

Last Updated: 2026-02-05 15:19:43

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

n 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 as well as reason formally about systems during development.

Content

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. 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 modeling and designing discrete transition systems. Here students will come to understand the difference between correct construction versus final validation. Our focus will include both background and applications. The background reviews logic, set theory, and a development framework for discrete transition model construction. The applications include the development of sequential, distributed, and concurrent programs as well as hardware systems and complete systems (e.g. embedded systems).

General Information

Language
English
Levels
BSC
Frequency
Yearly recurring

Examination

Type
end-of-semester examination

Course Components

Type Title Time & Place Hours
lecture Formal Methods and Functional Programming
  • Tue 08:15-11:00 (HG E 7)
  • 03.04 Date 11:15-13:00 (CAB H 57)
  • 27.04 Date 08:15-10:00 (HG E 1.2)
  • 27.04 Date 08:15-10:00 (HG E 7)
3 h weekly
exercise Formal Methods and Functional Programming
  • Wed 14:15-16:00 (ETF B 105)
  • Wed 14:15-16:00 (ETZ J 91)
  • Wed 14:15-16:00 (HG D 3.1)
  • Wed 14:15-16:00 (HG D 7.2)
  • Fri 08:15-10:00 (CLA E 4)
  • Fri 08:15-10:00 (IFW A 32.1)
  • Fri 08:15-10:00 (IFW A 34)
  • Fri 08:15-10:00 (IFW C 42)
2 h weekly

Offered In