Formal Methods and Functional Programming

Announcements

22/08/16 Please attend the exam in the appropriate room, based on your surname: 

• Surnames A-I: in HIL F 61
• Surnames J-Z: in HIL F 41

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
  Group 1: CAB G 52, English,
  Group 2: CHN D 46, German,
  Group 3: NO D 11, English,
  Group 4: NO E 11, English,
  
• Wednesday 13-15
  Group 5: CAB G 57, English,
  Group 6: CHN D 46, English, 
• Wednesday 15-17
  Group 7: CHN D 46, German,

)

Exams and Quizzes

There will be a session examination: to be held from 9:00 - 12:00 on 23rd August 2016. This examination covers both halves of the course. 

Surnames A-I: in HIL F 61
Surnames J-Z: in HIL F 41

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 10. The second one will take place on May 12.

Homework is optional, but highly recommended.

Quizzes on March 10 and May 12

• protected page Results of the first quiz
• protected page Results of the second quiz

Course Material

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

Submission Instructions

Haskell programs must be submitted electronically via codeboard.io. The relevant assignments mention the URL of the corresponding project on codeboard.io. Please follow the submission guidelines outlined in the first exercise sheet to ensure that we are able to identify your submission and provide feedback.

Other assignments (proofs, etc.) for the first part of the course can be submitted in two ways. The first way is to e-mail to your tutor. Please put [FMFP] in the subject of the message. The second way is to drop off your solution in the drop box inside CAB H 68. In that case, please mark your tutor name and exercise class (day) visibly on your submission.

All solutions must be received by 9:00 am on the Monday after the exercise is published, in order to receive feedback.

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.