Formal Methods and Functional Programming

Announcements

• Exam viewings:
  • Monday, 25. September, 14–16, CNB F110
  • Wednesday, 27. September, 14–16, CNB F110
• 21.7.: Date and place of the final exam have been published, see below
  
• 4.6.: Quiz 2, the master solution and the results are available from the secured course material website. The quiz can be reviewed on Thursday, 15.6. from 10:00 to 12:00 in CNB H 100.5.
• 18.5.: Updated Solution 11, Sheet 12 and Session 12: fixed several minor mistakes
  
• 11.5.: Updated Sheet 11: the URL in Assignment 4 now refers to codeboard.ethz.ch
  
• Submission instructions have been updated, see below
  
• Date and place of Quiz 2 have been published, see below
  
• The results of Quiz 1 have been mildly updated after the quiz viewing (if you were promised a higher number of points please check) 
• The results of Quiz 1 are online (see below)
• The first lecture takes place on 21.02.2017
  

Overview

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

Classes: Tuesday 10-12 HG E 5 and Thursday 10-12 HG E 5

Credits: 7 ECTS (4V + 2U)

Requirements: none

Language: English

Exercise Classes

• Tuesday 13-15
  CAB G 52, English,
  CHN D 46, English,
  NO D 11, German,
  NO E 11, English,
  
• Wednesday 15-17
  CHN D 42, English,
  CHN D 46, German,

For questions/issues concerned with the first half (Functional Programming), please e-mail Dr. Dmitriy Traytel (); for the second half (Formal Methods), please e-mail Dr. Malte Schwerhoff ().

Homeworks, Exams, and Quizzes

There will be a 180 minutes written examination on August 14 from 9:00 to 12:00 in HIL D 15 (last names starting with A-K) and HIL C 15 (L-Z). 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 will count 10% of the total grade. The first one will take place on March 21 at 10:10 in ML D 28 (last name starting with A–L) and HG E 5 (M–Z).

Here is protected pagequiz 1lock, its protected pagesolutionlock, and the protected pageresultslock. Moreover, protected pagethis histogramlock shows how many points (from 1.5 to 10) were earned by how many students. There will be two possibilities for students to view their results of quiz: together with the viewing of the final exam after the semester and on Thursday, 30.03.2017 from 9:15 to 10:15 (before the lecture) in (presumably) HG E 5.

The second quiz took place on May 9 at 10:10 in ML D 28 (last name starting with A–L) and HG E 5 (M–Z). Results are available from the secured course material website.

Homework is optional, but highly recommended.

Course Material

The lecture notes, slides, and other resources are available in our protected pagesecured arealock. To access the secured area, you must first login with your nethz account at the top right corner of the page.

New Submission Instructions

In the second half of the course, homework can be submitted in one of two ways:

• By email to the appropriate tutor (see above)
• By hand in the appropriate box inside (print) room CAB H 68

An exception are the (very) few Haskell exercises: these must be submitted via Codeboard (as before).

In order to receive feedback, solutions must be received by 09:00 on the Monday after the exercise sheet is published.

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.