This repository is the homepage of the course Formal Verification and hosts the material necessary for the labs.
- Professor: Viktor Kunčak
- Teaching Assistant: Sankalp Gambhir
- Student Assistant: Jacopo Philip Moretti
The grade is based on the labs, written midterm exam, 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% written midterm exam (see this folder with past exams)
- 20% total: 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
The midterm exam will be held on Thursday 27/11/2025, during the 15h-19h slot for the course, in rooms GR A3 30 and MED 0 1618. The exact time and seating plans will be communicated later.
The course 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. The projects must be presented with a written report as well as a live presentation of project results, answering our questions.
In this course, we introduce formal verification as a principled approach for developing systems that do what they are expected to.
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 2024 edition.
Note that slides can be found underneath each lecture video as attachments on the Mediaspace links 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 | 11.09.2025 | 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 | 12.09.2025 | 13:15 | DIA 004 | Lecture 3 | What is a Formal Proof? and Propositional Resolution | |
| 2 | Thu | 18.09.2025 | 15:15 | GRA330 | Lecture 4 PDF | continue Propositional Resolution and DPLL |
| Example: | Toy implementations of SAT solvers in Scala | |||||
| 17:15 | GRA330 | Lab 1 | ||||
| Fri | 19.09.2025 | 13:15 | DIA 004 | Exercises 1 | Propositional Logic | |
| Reading: | CalComp-Ch.1 ∨ HandAR-Ch.2 | |||||
| 3 | Thu | 25.09.2025 | 15:15 | GRA330 | Lecture 5 PDF | Automating First-Order Logic Proofs Using Resolution |
| 17:15 | GRA330 | Lab 2 | A communication protocol in Stainless | |||
| Reading: | HandAR-Ch.3 | |||||
| Fri | 26.09.2025 | 13:15 | DIA 004 | Exercises 2 | Traces, SAT, models | |
| 4 | Thu | 02.10.2025 | 15:15 | GRA330 | Lecture 6 PDF | Compactness and Term Models for First-Order Logic. Slides |
| 17:15 | GRA330 | Lab 3 | FOL Resolution | |||
| Provers Proved New Math Results (also in NYT), SPASS Prover on The Web | ||||||
| Reading: | HandAR-Ch.3 | |||||
| Fri | 03.10.2025 | 13:15 | DIA 004 | Exercises 3 | ||
| 5 | Thu | 09.10.2025 | 15:15 | GRA330 | Lecture 7: vcgen.pdf Hoare.pdf | Converting Imperative Programs to Formulas, Hoare Logic, Strongest Postcondition, Weakest Precondition |
| Fri | 10.10.2025 | 13:15 | DIA 004 | Exercises 4 | Transition Systems, Hoare Logic, Relations | |
| 15:15 | GRA330 | Lecture 8 PDF | Quantifier Elimination | |||
| 6 | Thu | 16.10.2025 | 17:15 | GRA330 | Lab 4 | Using Lisa Proof Framework |