Formal Methods and Functional Programming

Overview

Lecturers: Prof. Dr. David Basin and Dr. Alex Summers

Classes: Tuesday 10-12 HG F 3 and Thursday 10-12 HG F 1

Credits: 7 ECTS
Homework is optional, but highly recommended. There will be a session examination.

Exercise Classes (second part):

• Tuesday 16-18
  Stefan Heule HG G 26.5 (German, 16:15-18:00) - material for the tutorials
  Yannis Kassios CLA E 4 (English, 16:00-17:45)
  Malte Schwerhoff ETZ E 7 (German, 16:00-17:45)
  
• Wednesday 15:15-17:00
  Yannis Kassios IFW A 34 (English)
  Malte Schwerhoff IFW C 33 (German)
  

Please attend the same session as in the first half of the course. The students of Jérôme Dohrau should attend Malte Schwerhoff's session on Tuesday. The students who previously attended Ognjen Marić's session in IFW A 32.1 can attend any other session (Tue or Wed). If you wish to switch session/group, please email Yannis Kassios first.

Solutions can be submitted in two ways: you can either send them by email to the assistant assigned to you or submit them on paper in the appropriate box on the window sill in front of CAB F 53.1 Solutions must be received by 11:00am on the Monday after the exercise is published, in order to receive feedback.

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 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.

Announcements

The Q/A session for this course is arranged: day: Monday 5.8, time: 14:00-16:00, place: CAB G51

• 11 July: Correction: In the solutions of Sheet 12, Assignment 4, Case 2 (rule of consequence), there was a typo which may have caused confusion. In particular, in the two derivations that appear at the very bottom of the proof, (a) the symbols P and P' were swapped and (b) the symbols Q and Q' were swapped. The correct version has now been uploaded.
• 2nd June: In slide deck 10, the technique presented for "omega-regular liveness properties" actually applies to all LTL-specified properties (as was explained in the lecture). This has now been clarified in an updated version of the slides. The slides for the "Epilogue" are also now available online.
• 29th May: Exercise sheet 14 (question 4(b)) has been clarified - please see the updated version. Also, in slide deck 10, we renamed "prefix automata" to "bad-prefix automata", to avoid a terminology clash with other topics/courses.
• 28th May: Some mistakes were fixed in slide deck 10 ("true"/"false" instead of "valid"/"not valid", and the wrong example LTL property stated for some automata examples). Please see the updated version.
• 28th May: The notation for "indexing" in a computation/trace has been clarified, in slide deck 9 (Linear Time Properties). You may want the updated version.