ETH - InfSec - Formal Methods and Functional Programming

02.06.2008	Answers to questions: Andreas will answer your questions in IFW C42 on Friday, June 6, 13:00.
30.05.2008	Answers to questions: Matthias can come to ETH (IFW C47.2) at Saturday, June 7, 14:00, in order to answer questions. Please send him a mail, if you are interested.
23.05.2008	The final exam will take place on June 9th, 10:00 to 12:00 in CAB G11 (names starting with A-M) and CAB G61 (names starting with N-Z). Do not forget to bring your legi. The final exam will be a closed-book exam. However, you will be allowed to use the latest reference card, which will be distributed together with the exam questions.
14.05.2008	Updated this week's lecture slides (Mathematical Language and Proofs, slide numbers 76, 77, 101, 110, 112, 113, and 150).
9.05.2008	We will have the Course Evaluation for the FM part during next lecture on Tuesday, May 13th.
23.04.2008	Midterm results announced in the display case in IFW floor C. The post-exam review takes place on Wednesday, April 30th. Please go to Barbara Geiser's office (IFW C 49.1) or Benedikt Schmidt's office (IFW C43.2).
11.04.2008	Formal Methods part starting next Tuesday, Apr 15th
	Exercise sessions: please continue to go to the same exercise session (same time and place), as you did for the Functional Programming part. Only your assistant might change for the FM part, see below.

Overview

Lecturers: Dr. Felix Klaedtke and Dr. Christoph Sprenger

Classes: Tue 8-11, HG E 7

Exercises:

Wed 14-16
- HG D7.2 - Thai Son Hoang / Matthias Schmalz
Fri 8-10
- IFW A 32.1 - Matthias Schmalz
- IFW A 34 - Thai Son Hoang
- IFW B 42 - Maria Husmann
- IFW C 42 - Andreas Kaegi

Notes:

Solutions on paper can be handed in during the lecture breaks.
Exercise groups: exercise_groups_fm.txt

Credits: 6

There will be a mid-term and a final exam. More details to come.

Homework is optional, but highly recommended.

Exams:

Midterm: April 11th (Fri 8-10), 2008
Final: June 9th (Mon 10-12), 2008

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 modeling and designing discrete transition systems. Here students will come to understand the difference between correct construction versus final validation. Our focus will include both background and applications. The background reviews logic, set theory, and a development framework for discrete transition model construction. The applications include the development of sequential, distributed, and concurrent programs as well as hardware systems and complete systems (e.g. embedded systems).

Resources

Literature:

Graham Hutton. Programming in Haskell. Cambridge University Press. 2007
Simon Thompson. Haskell: The Craft of Functional Programming. Addison-Wesley, 1996
Harold Abelson and Gerald Jay Sussman with Julie Sussman. Structure and Interpretation of Computer Programs. MIT Press, 1996. (full version online)

Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
folgender Seite.

Important Note:
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.
More information

!!! Dieses Dokument stammt aus dem ETH Web-Archiv und wird nicht mehr gepflegt !!!
!!! This document is stored in the ETH Web archive and is no longer maintained !!!