Formal Methods and Functional Programming
Spring Semester 2023, Bachelor course (252-0058-00)
Overview
Lecturers: Prof. Dr. Peter Müller and Prof. Dr. David Basin
Classes: Tuesdays 10-12 and Thursdays 10-12
Credits: 7 ECTS (4V + 2U)
Language: English (lectures), English and German (exercises)
Exercise classes: Tuesdays 14-16, Wednesdays 10-12 or Wednesdays 16-18
For questions/issues concerned with the first half (Functional Programming), please contact François Hublet; for the second half (Formal Methods), please contact Jonáš Fiala.
Announcements
- [2023/05/20] The master solution for the second midterm is now available protected pageherelock. Your recorded answers and points can be found protected pageherelock.
- [2023/05/04] Friendly reminder: next week, on Thursday, May 9 from 10:15 to 10:45, the second midterm quiz will take place in the usual lecture halls. All content up to slide 72 is relevant for the exam.
- [2023/04/18] There will be a few recap sessions this week: Tu 14-16 NO D 11 (German), We 16-18 HG G 26.5 (English), We 16-18 CHN D 42 (German)... (more TBA) You can attend any of them.
- [2023/04/06] After the Spring holidays, Prof. Müller's group is taking over. Contact Jonáš Fiala for details.
- [2023/03/30] The master solution & feedback of the first midterm are out! For those of you who participated, you should have received your grade by e-mail today.
- [2023/03/06] Friendly reminder: next week, on Thursday, March 16 from 10:15 to 10:45, the first midterm quiz will take place in the usual lecture halls. All content from weeks 1-3 is relevant for the exam.
- [2023/02/21] More spots have been open in various exercise classes. If you could not register so far, please try again.
- [2023/02/20] The course material for week 1 is online! Do not forget to check CodeExpert.
- [2023/01/27] The course webpage for this year's FMFP is up and running! Please enroll in an exercise group.
Course material
Semantics Summary
- [2023/05/25] DownloadIMP Syntax summary (PDF, 138 KB)vertical_align_bottom
- [2023/05/25] DownloadNatural Semantics (Big Step) summary (PDF, 128 KB)vertical_align_bottom
- [2023/05/25] DownloadStructural Operational Semantics (Small Step) summary (PDF, 126 KB)vertical_align_bottom
- [2023/05/25] DownloadAxiomatic Semantics (Hoare Logic) summary (PDF, 113 KB)vertical_align_bottom
Week 15
- [2023/05/31] DownloadHomework 14 (PDF, 147 KB)vertical_align_bottom (due June 7) - Downloadsolution (PDF, 130 KB)vertical_align_bottom
- [2023/05/31] DownloadOptional homework (PDF, 128 KB)vertical_align_bottom
Week 14
- [2023/05/18] DownloadHomework 13 (PDF, 115 KB)vertical_align_bottom (due May 30/31) - Downloadsolution (PDF, 122 KB)vertical_align_bottom
- [2023/05/09] DownloadOptional homework (PDF, 195 KB)vertical_align_bottom
- [2023/05/25] DownloadExercise session 14 (PDF, 124 KB)vertical_align_bottom (without solutions)
- [2023/05/31] DownloadExercise session 14 (PDF, 146 KB)vertical_align_bottom (with solutions)
- [2023/05/25] DownloadSlides: Linear Temporal Logic (PDF, 303 KB)vertical_align_bottom
- [2023/05/30] DownloadSlides: Model Checking (PDF, 269 KB)vertical_align_bottom
Week 13
- [2023/05/18] DownloadHomework 12 (PDF, 106 KB)vertical_align_bottom (due May 23/24) - Downloadsolution (PDF, 176 KB)vertical_align_bottom
- [2023/05/09] DownloadOptional homework (PDF, 146 KB)vertical_align_bottom
- [2023/05/22] DownloadExercise session 13 (PDF, 137 KB)vertical_align_bottom (without solutions)
- [2023/05/25] DownloadExercise session 13 (PDF, 211 KB)vertical_align_bottom (with solutions)
Week 12
- [2023/05/09] DownloadHomework 11 (PDF, 97 KB)vertical_align_bottom (due May 16/17) - Downloadsolution (PDF, 159 KB)vertical_align_bottom
- [2023/05/09] DownloadOptional homework (PDF, 227 KB)vertical_align_bottom
- [2023/05/04] DownloadExercise session 12 (PDF, 119 KB)vertical_align_bottom (without solutions)
- [2023/05/04] DownloadExercise session 12 (PDF, 185 KB)vertical_align_bottom (with solutions)
- [2023/05/04] DownloadSlides: Modeling (PDF, 330 KB)vertical_align_bottom
Week 11
- [2023/04/20] DownloadHomework 10 (PDF, 118 KB)vertical_align_bottom (due May 9/10) - Downloadsolution (PDF, 171 KB)vertical_align_bottom
- [2023/04/20] DownloadOptional homework (PDF, 143 KB)vertical_align_bottom
- [2023/05/04] DownloadExercise session 11 (PDF, 107 KB)vertical_align_bottom (without solutions)
- [2023/05/10] DownloadExercise session 11 (PDF, 167 KB)vertical_align_bottom (with solutions)
- [2023/05/04] DownloadSlides: Axiomatic Semantics (PDF, 299 KB)vertical_align_bottom
Week 10
- [2023/04/20] DownloadHomework 9 (PDF, 137 KB)vertical_align_bottom (due May 2/3) - Downloadsolution (PDF, 135 KB)vertical_align_bottom
- [2023/04/27] DownloadExercise session 10 (PDF, 130 KB)vertical_align_bottom (without solutions)
- [2023/05/04] DownloadExercise session 10 (PDF, 204 KB)vertical_align_bottom (with solutions)
Week 9
- [2023/04/27] DownloadExercise session 9 (PDF, 179 KB)vertical_align_bottom
- [2023/04/25] DownloadSlides: Operational Semantics (PDF, 383 KB)vertical_align_bottom
Week 8 (Formal methods starts!)
- [2023/04/17] DownloadSlides: Introduction (PDF, 361 KB)vertical_align_bottom
- [2023/04/17] DownloadSlides: Introduction to Language Semantics (PDF, 191 KB)vertical_align_bottom
Week 7
- [2023/04/06] protected pageExercise session slideslock
- [2023/04/04] protected pageSlides: monadslock
- [2023/04/04] protected pageExercise sheet 7lock - protected pageSolutionlock
Week 6
- [2023/04/04] protected pageExercise session slideslock
- [2023/03/27] protected pageSlides: case studieslock
- [2023/03/27] protected pageExercise sheet 6lock - protected pageSolutionlock
Week 5
- [2023/03/27] protected pageExercise sessions slideslock
- [2023/03/27] protected pageSlides: lazy evaluationlock
- [2023/03/20] protected pageExercise sheet 5lock - protected pageSolutionlock
Week 4
- [2023/03/14] protected pageCYP referencelock
- [2023/03/13] protected pageLast year's midtermlock - protected pageSolutionlock
- [2023/03/16] protected pageMidtermlock - protected pageSolutionlock - protected pageGeneral feedbacklock
- [2023/03/16] protected pageExercise sessions slideslock
- [2023/03/13] protected pageSlides: algebraic data typeslock
- [2023/03/13] protected pageSlides: moduleslock
- [2023/03/13] protected pageExercise sheet 4lock - protected pageSolutionlock
Week 3
- [2023/03/09] protected pageExercise sessions slideslock
- [2023/03/06] protected pageSlides: higher-order programming and typeslock
- [2023/03/06] protected pageExercise sheet 3lock - protected pageSolutionlock
Week 2
- [2023/03/02] protected pageExercise session slideslock
- [2023/03/06] protected pageSlides: correctnesslock
- [2023/02/24] protected pageSlides: listslock
- [2023/02/27] protected pageExercise sheet 2lock - protected pageSolutionlock
Week 1
- [2023/02/23] protected pageExercise session slideslock
- [2023/02/21] protected pageSlides: introductionlock
- [2023/02/21] protected pageSlides: natural deductionlock
- [2023/02/20] protected pageExercise sheet 1lock - protected pageSolutionlock
General Information
Course material:
All the course material will be uploaded on this website.
For the first part of the course, we will also use CodeExpert for programming exercises.
Lectures:
The lecture will be held in HG E 7. If not all students fit into the room, there will be a live streaming of the lecture in HG E 3. Please come to HG E 7 first.
Attendance is strongly recommended. No recordings will be provided.
Exercise Sessions:
Please enroll in an exercise group via Code Expert.
It is important you attend the same exercise group you are enrolled in Code Expert!
Tuesdays 14-16:
Group 1: CAB G 52 [English]
Group 2: CAB G 57 [German]
Group 3: NO D 11 [German]
Wednesdays 10-12:
Group 4: CAB G 52 [English]
Group 5: ETZ F 91 [English]
Group 6: HG E 33.5 [English]
Group 7: LEE C 114 [German]
Wednesdays 16-18:
Group 8: CHN D 42 [German]
Group 9: CHN F 46 [German]
Group 10: HG G 26.5 [English]
Exam and Quizzes:
There will be a 180 minutes written examination. This examination covers both halves of the course. Note that the examination is only offered in the session after the course unit.
There will also be two graded midterm quizzes. Each quiz will be 30 minutes and each may improve the final grade.
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.
Resources
Literature for the first part
- Miran Lipovača. external pageLearn you a Haskell for great good!call_made no starch press, 2011 (external pagefull version onlinecall_made)
- Simon Thompson. external pageHaskell: the Craft of Functional Programmingcall_made, Addison Wesley, 2011
- O'Sullivan, Stuart, Goerzen. external pageReal World Haskellcall_made, O'Reilly, 2008 (external pagefull version onlinecall_made)
- Graham Hutton. external pageProgramming in Haskellcall_made. Second edition, Cambridge University Press, 2016
- Mordechai Ben-Ari. external pageMathematical Logic for Computer Sciencecall_made. Springer, 2012
Haskell links
The external pageZurich Haskell user groupcall_made maintains a collection of external pageHaskell linkscall_made useful for both Haskell beginners and experts.
Proof checker
The proof checker CYP for induction proofs is external pageavailable on GitHubcall_made.
Literature for the second part
- Hanne Riis Nielson and Flemming Nielson. external pageSemantics with Applications: A Formal Introductioncall_made, John Wiley & Sons, 1992
- Christel Baier and Joost-Pieter Katoen. external pagePrinciples of Model Checkingcall_made. The MIT Press, 2008
Additional literature for interested students
- Chris Okasaki. Purely Functional Data Structures. Cambridge University Press, 1998.
- Harold Abelson and Gerald Jay Sussman with Julie Sussman. Structure and Interpretation of Computer Programs. MIT Press, 1996. (external pagefull version onlinecall_made)