Lecture: Formal Methods and Functional Programming

Bachelor Course 252-0058-00L, Spring Semester 2010

Announcements

• You can inspect your final exams on Thu, 16.9.2010, 10:00 - 11:00 in RZ F 5 and on Tue, 21.9.2010, 10:00 - 11:00 in RZ F 5. The course assistants will be present in case you have any questions.
  
  
• For those of you who want to install Spin/XSpin on Windows, you may find the following version of gcc useful. Disclaimer: we make no guarantees about it. However, I've personally found that it worked for me. You can find it here.
  
  
• The results of the lecturer evaluation for the course are now available here: both for the first half and for the second half of the course.
  
  
• There was a mistake on sheet 12, in the code for question 3. Apologies - please find a corrected version online. The solutions to sheet 11 are also now available.
  
  
• A Q & A session concerning the final exam will take place on Thu, 3.6.2010, 10:00 - 12:00 in HG F 7 (i.e., at the usual lecture time and place).
  Please consider what kind of questions/examples/topics you would like us to cover, and email your requests to Alex Summers, preferably by Tue, 1.6.2010

• The points achieved in the midterm exam can be found in the glass cabinet in front of CAB F 55.2.

• You can inspect your exam on Tue. 27th of April, 10:00-16:00 and on Thu., 6th of May 10:00-16:00. Please go to Barbara Geiser in CNB F 104.

• For the second half of the course, students should continue to attend exercise sessions at the same times and in the same rooms as for the first half. Note that exercises should be submitted in a different way (see "Exercises" below).
  
  
• Several of the exercise sessions which were in German for the first half of the course will be in English for the second half. If this is a problem for you then please email Alex Summers and explain your situation.
  
  
• The final exam will take place on Thu, 10.6.2010, 09:00 - 11:00
  in HG F5 for students A.. - Meier and
  in HG F7 for students Messmer - Z.. .
  
  
• The midterm exam will take place on Wed, 14.4.2010, 15:45 - 17:45
  in HG F1 for students A.. - Meier and
  in HG F7 for students Messmer - Z.. .
  The students may enter the exam room at 15:30.
  
  
• A Q & A session concerning the midterm exam takes place on Tue, 13.4.2010, 16:15 - 18:00 in IFW A 36. The slides from the session can be downloaded.
  
  
• The assignments to exercise sessions are as follows: group-assignment.txt.
  

Overview

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

Classes: Tue 9-11 in HG E 7, Thu 10-12 in HG F 7

Exercises:

(second half of the course)

• Tue 16-18
  
  • IFW C 42 (Alex Summers, English)
  • IFW B 42 (Yannis Kassios, English)
  • IFW A 34 (Malte Schwerhoff, German)
• Wed 15-17
  • IFW A 32.1 (Alex Summers, English)
  • IFW B 42 (Yannis Kassios, English)

  Solutions can be submitted in one of two ways. Either send them by email to the appropriate assistant, or submit them by hand in the appropriate box which will be located at the end of the corridor outside room RZ F1. In either case, solutions must be received by 9:15am on the Monday after the exercise is published, in order to receive feedback (which will be given in the exercise sessions that week).

(first half of the course - now completed)

• Tue 16-18
  
  • IFW C 42 (Martin Schaub, german)
  • IFW B 42 (Benedikt Schmidt, english, material for tutorial)
  • IFW A 34 (Simon Meier, german, material for tutorial)
• Wed 15-17
  • IFW A 32.1 (Christoph Sprenger, german, material for tutorial)
  • IFW B 42 (Adrian Kyburz, german)

Credits: 7

Homework is optional, but highly recommended. There will be a midterm and a final exam. The grade in the course will be determined based on the average points received in the midterm and the final exam.

Requirements: none

Language: English

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 modeling 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 analyze 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 modeled 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.

Resources

Literature for the second part:

• Hanne Riis Nielson and Flemming Nielson. Semantics with Applications: A Formal Introduction, John Wiley & Sons, 1992 (full version online)
  
• Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press. 2008
  

Literature for the first part:

• O'Sullivan, Stuart, Goerzen. Real World Haskell, O'Reilly, 2008 (full version online)
  
• Graham Hutton. Programming in Haskell. Cambridge University Press. 2007
  
• Simon Thompson. Haskell: The Craft of Functional Programming. Addison-Wesley, 1996

Additional literature for interested students:

• Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998. (partially online)
  
• Harold Abelson and Gerald Jay Sussman with Julie Sussman. Structure and Interpretation of Computer Programs. MIT Press, 1996. (full version online)

Course Material: here