This repository is the homepage of the course Formal Verification and hosts the material necesary for the labs.
- Professor: Viktor Kunčak
- Teaching Assistant: Simon Guilloud
- Student Assistant: Dario Halilovic
The grade is based on the written mid-term, as well as code, documentation, and explanation of projects during the semester. Specific percentages will be communicated in the first class and posted here.
The types of graded materials will include:
- 40% Late mid-term written exam in November (see this folder with past exams)
- 20% total: four-five labs, to be done in groups, each group working independently on same projects
- 40% final project to be done in groups, you will choose a topic with our agreement
- 10% Written presentation of a background paper
- 10% Results accomplished (how hard it was, how far you got)
- 10% Presentation of results
- 10% Final report
In this course we introduce formal verification as a principled approach for developing systems that do what they should do.
The course has two aspects:
- learning the practice of formal verification - how to use tools to construct verified software
- understanding the principles behind formal verification and the ways in which verification tools work
The course will follow a similar structure to the 2023 edition. Project can be a case study in developing a verified piece of software, an implementation of verification tool functionality, or a theoretical result about verification, constraint solving or theorem proving. Students present their projects with a written report as well as by a live presentation of project results, answering our questions.
Note that slides can be found underneath each lecture video on switch tube linkes below.
- [CalComp] The Calculus of Computation - Decision Procedures with Applications to Verification, 2007, from Springer, from EPFL library, by Aaron Bradley and Zohar Manna.
- [HandMC] Handbook of Model Checking, 2018, from from Springer, from EPFL Library, edited by Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem.
- [HandAR] Handbook of Practical Logic and Automated Reasoning, 2009, from Cambridge University Press and from EPFL Library, by John Harrison
In the reading list below, HandAR-Ch.2 means Chapter 2 in the Handbook of Practical Logic and Automated Reasoning Above, whereas HandMC-Ch.9 means Chapter 9 of the Handbook of Model Checking, etc.
To see the material, please visit https://mediaspace.epfl.ch , log in with your EPFL credentials and select this channel. Slides and listings are attached underneath the videos.
| Week | Day | Date | Time | Room | Topic | Videos & Slides |
|---|---|---|---|---|---|---|
| 1 | Thu | 12.09.2024 | 15:15 | GRA330 | Lecture 1 | Intro to FV, Intro to Stainless, Auxiliary Assertions, Unfolding, Disasters, Successes, and Inductive Invariants |
| 17:15 | GRA330 | Lecture 2 | Dispenser Example, Finite Systems Expressed with Formulas | |||
| Reading: | HandMC-Ch.10 | |||||
| Follow: | Stainless Tutorial Videos and materials | |||||
| Fri | 13.09.2024 | 13:15 | INR219 | Lecture 3 | What is a Formal Proof? and Propositional Resolution | |
| 2 | Thu | 19.09.2024 | 15:15 | GRA330 | Lecture 2 | continue Propositional Resolution |
| 17:15 | GRA330 | Lab 1 | ||||
| Fri | 20.09.2024 | 13:15 | INR219 | Exercises 1 | Propositional Logic | |
| Thu | 26.09.2024 | 15:15 | GRA330 | |||
| 17:15 | GRA330 | Lab 2 | A communication protocol in Stainless | |||
| Fri | 27.09.2024 | 13:15 | INR219 | Exercises 2 | Traces, SAT, models | |
| Thu | 03.10.2024 | 15:15 | GRA330 | |||
| 17:15 | GRA330 | |||||
| Fri | 04.10.2024 | 13:15 | INR219 | |||
| Thu | 10.10.2024 | 15:15 | GRA330 | |||
| 17:15 | GRA330 | |||||
| Fri | 11.10.2024 | 13:15 | INR219 | |||
| Thu | 17.10.2024 | 15:15 | GRA330 | |||
| 17:15 | GRA330 | |||||
| Fri | 18.10.2024 | 13:15 | INR219 | |||
| Thu | 24.10.2024 | 15:15 | Holidays | |||
| 17:15 | Holidays | |||||
| Fri | 25.10.2024 | 13:15 | Holidays | |||
| Thu | 31.10.2024 | 15:15 | GRA330 | |||
| 17:15 | GRA330 | |||||
| Fri | 01.11.2024 | 13:15 | INR219 | |||
| Thu | 07.11.2024 | 15:15 | GRA330 | |||
| 17:15 | GRA330 | |||||
| Fri | 08.11.2024 | 13:15 | INR219 | |||
| Thu | 14.11.2024 | 15:15 | GRA330 | |||
| 17:15 | GRA330 | |||||
| Fri | 15.11.2024 | 13:15 | INR219 | |||
| Thu | 21.11.2024 | 15:15 | GRA330 | |||
| 17:15 | GRA330 | |||||
| Fri | 22.11.2024 | 13:15 | INR219 | |||
| Thu | 28.11.2024 | 15:15 | GRA330, AAC114 | Midterm, until 18:00 | ||
| Fri | 29.11.2024 | 13:15 | INR219 | |||
| Thu | 05.12.2024 | 15:15 | GRA330 | |||
| 17:15 | GRA330 | |||||
| Fri | 06.12.2024 | 13:15 | INR219 | |||
| Thu | 12.12.2024 | 15:15 | GRA330 | |||
| 17:15 | GRA330 | |||||
| Fri | 13.12.2024 | 13:15 | INR219 | |||
| Thu | 19.12.2024 | 15:15 | GRA330 | |||
| 17:15 | GRA330 | |||||
| Fri | 20.12.2024 | 13:15 | INR219 |
Midterm exam: Thursday, 28 November, 15:00-18:00