Formal Methods and Functional Programming

Overview

Lecturers: Prof. Dr. David Basin and Prof. Dr. Peter Müller

Classes: Tuesday 10-12 HG F 3 and Thursday 10-12 HG F 1

Credits: 7
Homework is optional, but highly recommended. There will be a session examination.

Exercise Classes (updated for second half of the course):

• Tuesday 16-18:
  HG D 3.1 (Malte Schwerhoff, German)
  HG G 26.5 (Yannis Kassios, English)
• Wednesday 15-17:
  IFW A 34 (Yannis Kassios, English)
  IFW A 32.1 (Alex Summers, English)
  IFW C 33 (Malte Schwerhoff, German)

Please attend the same session as in the first half of the course (the rooms and times are unchanged). If you want to switch session/group (for language reasons), please email Malte Schwerhoff.

Solutions can be submitted in two ways: you can either send them by email to the assistant assigned to you or submit them on paper in the appropriate box on the window sill in front of CAB F 51.1 Solutions must be received by 10:15 on the Monday after the exercise is published, in order to receive feedback.

Requirements: none

Language: English

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 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 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.