Formal Methods and Functional Programming

Announcements

• The final exam on Saturday, August 17 will take place in two rooms. Please be ready in front of your assigned room shortly before 9:00 am.
  
  Students with last names A-Ma go to HIL F 41.
  Students with last names Me-Z go to HIL F 61.
• The protected page first and the protected page second midterm quiz are available on the course webpage.
• Q&A session: Tuesday, July 30, at 10:00 in CAB G 52
  
• The protected page results of second midterm quiz are online. You can review your quiz on Thursday, June 6, between 8:30am and 10:00am in CAB J 71.6. There will be a second review toghether with the final exam after the examination session.
• The second midtern quiz on May 9 will take place in four different rooms. Please be ready in front of your assigned room by 10:05 am.
  
  Students with last names A - J go to HG G 5.
  Students with last names K - Lo go to CHN E 46.
  Students with last names Lu - M go to CHN F 46.
  Students with last names N - Z go to HG E 3.
• All competition results, discussions, and the art gallery have been uploaded.
  
• The last competition task is online. Please note that the deadline is on Tuesday, 2nd April, 23:59 CEST.
  
• The game week has started! Please submit your strategy until the extended deadline on Tuesday, 2nd April, 23:59 CEST, and win a special prize.
  
• The results, discussion, and a pair of follow-up exercises for the third and fourth competition task are online.
• The protected page results of Quiz 1 are online. You can review your quiz on Thursday, March 21, between 8:30 and 10:00 in CNB F 110. There will be a second review together with the final exam after the examination session.
• The second midterm quiz will take place on May 9 during the lecture.
• The results and discussion of the second competition task are online.
• The results and discussion of the first competition task are online.
• Please register for the exercise classes.

Overview

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

Classes: Tuesday 10–12 and Thursday 10–12, HG G 5

Credits: 7 ECTS (4V + 2U)

Requirements: none

Language: English

Exercise classes:

• Tuesday 13–15
  CAB G 52, Martin Clochard (, English)
  CHN D 46, Mauro Bringolf (, German)
  NO D 11, Felix Wolf (, German)
  NO E 11, Gaurav Parthasarathy (, English)
  
• Wednesday 15–17
  CAB G 59, Jan Veen (, German)
  CHN D 42, Sandra Dünki (, German)
  IFW C 33, Arshavir Ter-Gabrielyan (, English)
  
• Feedback only
  Jérôme Dohrau (, English/German)

For questions/issues concerned with the first half (Functional Programming), please e-mail Joshua Schneider (); for the second half (Formal Methods), please e-mail Jérôme Dohrau ().

Homeworks, Exams, 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.

This year, there will also be two graded midterm quizzes. Each quiz will be 30 minutes and each may improve the final grade. The first one took place on March 12 at 10:15 (protected page results). The second quiz will take place on May 9 during the lecture.

Homework is optional, but highly recommended.

A functional programming competition runs during the first seven weeks of the course and is reported on here.

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.