Formal Methods and Functional Programming

Announcements

• The review sessions for the FMFP exam (where you can come look at your exam) take place on the following days:
  - Thursday 23 September from 16h30 to 18h00 in CAB G56
  - Friday 24 September from 12h00 to 13h30 in CAB G52
  
 
• The final exam will take place on Monday, August 16th from 8h30 to 11h30. You are assigned to one of two rooms according to the first letter of your last name:
  -  Students with last names A -Ri : HIL G41
  -  Students with last names Ro-Z : HIL G61

• We have uploaded the protected page cheat sheet that will be provided at the exam.
  
• The protected page grades of the two midterms are available.
  
• The protected page solution of the second quiz is available on the course webpage.
  
• If you encounter some issues with the most recent version of Viper in VSCode, try to switch back to version 2.2.3 and disable automatic updates.
• We added to the secured area the instructions to access the quiz.
• The second mock quiz takes place on Tuesday, May 11th at 12h00.
  
• The second quiz takes place on Tuesday, May 18th at 10h15. The quiz will be conducted on Moodle. The exercises will be made available at 10h15 and you will then have exactly 30 minutes to submit the answers.
  
• The first quiz takes place on Tuesday, March 16th at 10h15. The quiz will be conducted directly on Code Expert. The exercises will be made available at 10h15 and you will then have exactly 30 minutes to submit the answers.
• The deadline for the Code Expert assignments of Week 3 has been shifted. The new deadline is Monday, 15th of March, at 23:59.
• Please enroll in the exercise class that you plan to attend.
• The first lecture is on Tuesday, February 23. There will be an exercise class in the first week. 
• Lectures and exercise classes will be held online, via zoom. All zoom links are posted in the Secured Area. 

Overview

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

Classes: Tuesdays 10-12 and Thursdays 10-12

Credits: 7 ECTS (4V + 2U)

Requirements: none

Language (lecture): English

Exercise classes for the Functional Programming part: 

• Tuesdays 14–16: 
  CAB G52: (German)
  CAB G57: (German)
  ETZ G91: (German)
  NO D11 : (English)
  NO E11: (English)

• Wednesdays 16–18:
  CHN D42: (German)
  HG G26.5: (German)
  CHN F46:  (English)
  NO E11: (English)

Exercise classes for the Formal Methods part:

• Tuesdays 14–16:
  (English)
   (English)
  (English)
  (German)
  (German)
  

• Wednesdays 16–18:
  (English)
  (German)
  (German)
  (English)
  

Note that rooms are listed only in case ETH regulations will allow to return to partial presence teaching later in the semester.

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

Student Forum : https://moodle-app2.let.ethz.ch/course/view.php?id=14733
Please use the Moodle forum as main plaftorm for asking questions!

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.

There will also be two graded midterm quizzes. Each quiz will be 30 minutes and each may improve the final grade.
The first quiz will take place on March 16th and will be an online programming quiz. 

Homework is optional, but highly recommended.

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.