ETH Zuerich - Homepage
Information Security

Lecture: Formal Methods and Functional Programming

Master in Information Security

For more information about the Information Security Master Track visit:

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


June 29th 2009 You can find your grades now in the showcase in front of the room IFW C42.    
June 29th 2009 You can inspect your exam on the following dates: Thu. July 2nd, Fri. July 10th, Tue. July 14th between 10:00 to 12:00. Please go to Barbara Geiser at IFW C49.1.    


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

Classes: Tue 9-12, HG E 7


Credits: 6

Homework is optional, but highly recommended. There will be a midterm and a final exam. If somebody fails the course, a repetition exam consisting of new exams for both parts can be taken.


Requirements: none

Language: English


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.


Literature for the first part:

Literature for the second part:

Additional literature for interested students:

Course Material: here


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

© 2011 ETH Zurich | Imprint | Disclaimer | 29 June 2009