Formal Methods and Functional Programming

Overview

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

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, Wednesdays 10-12 or Wednesdays 16-18

For questions/issues concerned with the first half (Functional Programming), please contact François Hublet; for the second half (Formal Methods), please contact Jonáš Fiala.

Announcements

• [2023/05/20] The master solution for the second midterm is now available protected page here. Your recorded answers and points can be found protected page here.
  
• [2023/05/04] Friendly reminder: next week, on Thursday, May 9 from 10:15 to 10:45, the second midterm quiz will take place in the usual lecture halls. All content up to slide 72 is relevant for the exam.
  
• [2023/04/18] There will be a few recap sessions this week: Tu 14-16 NO D 11 (German), We 16-18 HG G 26.5 (English), We 16-18 CHN D 42 (German)... (more TBA) You can attend any of them.
  
• [2023/04/06] After the Spring holidays, Prof. Müller's group is taking over. Contact Jonáš Fiala for details.
  
• [2023/03/30] The master solution & feedback of the first midterm are out! For those of you who participated, you should have received your grade by e-mail today.
  
• [2023/03/06] Friendly reminder: next week, on Thursday, March 16 from 10:15 to 10:45, the first midterm quiz will take place in the usual lecture halls. All content from weeks 1-3 is relevant for the exam.
  
• [2023/02/21] More spots have been open in various exercise classes. If you could not register so far, please try again.
  
• [2023/02/20] The course material for week 1 is online! Do not forget to check CodeExpert.
  
• [2023/01/27] The course webpage for this year's FMFP is up and running! Please enroll in an exercise group.
  

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.